proposition: Theorem sum_even : forall n p:nat, even n -> even p -> even (n+p).
proof: Proof. intros n p Heven_n; induction Heven_n. - trivial. - intro H0; simpl; constructor; auto. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector