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