proposition: Lemma even_opp : forall n, even (-n) = even n.
proof: Proof. assert (H : forall n, Even n -> Even (-n)). { intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv. } intros n. rewrite eq_iff_eq_true, !even_spec. split. - rewrite <- (opp_involutive n) at 2. apply H. - apply H. Qed.
imports: Bool ZMulOrder NZParity