proposition: Lemma even_prod : forall p q, Nat.Even ((p + q + 1) * (p + q)).
proof: Proof. intros p q; destruct (Even_or_Odd (p + q)). - destruct H as [m Hm]; rewrite Hm; exists ((2 * m + 1) * m); ring. - destruct H as [m Hm]; rewrite Hm; exists ((m + 1) * (2 * m + 1)); ring. Qed.
imports: Coq(Arith Lia )