In: Advanced Math
4. Prove that the universal quantifier distributes over conjunction, using constructive logic,
(∀x : A, P x ∧ Qx) ⇐⇒ (∀x : A, P x) ∧ (∀x : A, Qx) .
6. We would like to prove the following statement 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 predicate logic.
b. Provide the antecedent required for a proof by contraposition for the given statement.
c. Provide the consequent for a proof by contraposition for the given statement.
d. Prove the contrapositive statement is true, from which you can conclude that the original statement is true. You may use either Coq or the informal proof shown in the text.