proposition: Theorem plus_2_even_inv' : forall n:nat, even (S (S n))-> even n.
proof: Proof. intros n H. generalize (refl_equal (S (S n))); pattern (S (S n)) at -2. induction H. - discriminate. - intros H0 ; injection H0; intro; now subst n0. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector