proposition: Lemma even_spec n : even n = true <-> Even n.
proof: Proof. unfold Even. zify. rewrite Z.even_spec. split; intros (m,Hm). - exists (of_Z m). now zify. - exists [m]. revert Hm. now zify. Qed.
imports: Bool ZArith OrdersFacts Nnat ZAxioms ZSig Lia