proposition: Lemma parity_mismatch_not_eq:forall m n, Nat.Even_alt m -> Nat.Odd_alt n -> m <> n.
proof: Proof. intros m n H_even H_odd H_eq; subst m. apply Nat.Even_alt_Even in H_even. apply Nat.Odd_alt_Odd in H_odd. apply (Nat.Even_Odd_False n); trivial. Defined.
imports: Coq(ZArith) Coq(Lia)