5. Contrapositive

EasyProofFree10 points

Given h : P → Q, prove ¬Q → ¬P. Remember that ¬P means P → False.

Solution.lean

1theorem solution (P Q : Prop) (h : P → Q) : ¬Q → ¬P := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

P Q:Prop

h:P → Q

⊢¬Q → ¬P

ReadyLn 1, Col 1Lean 4

Draft saved in this browser