proposition: Lemma even_spec n : even n = true <-> Even n.
proof: Proof. unfold Even. zify. rewrite Z.even_spec. split; intros (m,Hm). - exists (N_of_Z m). zify. rewrite spec_N_of_Z; trivial. omega_pos n. - exists [m]. revert Hm; now zify. Qed.
imports: ZArith OrdersFacts Nnat NAxioms NSig Lia