Anonymous user
Proof: Difference between revisions
m
→{{header|Coq}}: simplify proof
(→{{header|Coq}}: complete solution) |
m (→{{header|Coq}}: simplify proof) |
||
Line 319:
Goal forall n m, even n -> even m -> odd (n + m) -> False.
Proof.
intros ? ? en em onpm.
▲ assert (Hx := even_plus_even _ _ H H0). simpl in Hx.
Qed.
| |||