proposition: Lemma double_S_neq_pred:forall m n, ~Nat.double (S m) = pred (Nat.double n).
proof: Proof. intros m [|n]. unfold Nat.double; lia. apply (parity_mismatch_not_eq (Nat.double (S m)) (pred (Nat.double (S n)))); try apply even_double; replace (pred (Nat.double (S n))) with (S (Nat.double n)); [ constructor; apply even_double | unfold Nat.double; lia]. Defined.
imports: Coq(ZArith) Coq(Lia)