4. Prove that the universal quantifierdistributes over conjunction, using constructive logic,
(∀x : A, P x ∧ Qx) â‡â‡’ (∀x : A, P x) ∧ (∀x : A, Qx) .
6. We would like to prove the followingstatement by contraposition, For all natural numbers x and y, if x+ y is odd, then x is odd or y is odd.
a. Translate the statement into a statement of predicatelogic.
b. Provide the antecedent required for a proof by contrapositionfor the given statement.
c. Provide the consequent for a proof by contraposition for thegiven statement.
d. Prove the contrapositive statement is true, from which youcan conclude that the original statement is true. You may useeither Coq or the informal proof shown in the text.