proposition: Lemma even_plus_n_n : forall n : nat, Nat.Even (n + n).
proof: Proof. intros n; replace (n + n) with (Nat.double n) by reflexivity. now rewrite Nat.double_twice; exists n. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)