proposition: Lemma odd_spec n : odd n = true <-> Odd n.
proof: Proof. unfold Odd. zify. rewrite Z.odd_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