proposition: Theorem spec_odd: forall x, odd x = Z.odd [x].
proof: Proof. intros x. unfold odd. assert (H := spec_even_aux x). symmetry. rewrite (Z.div_mod [x] 2); auto with zarith. destruct (even x); rewrite H, ?Z.add_0_r; simpl negb. apply not_true_is_false. rewrite Zodd_bool_iff. apply Zeven_not_Zodd. apply Zeven_2p. apply Zodd_bool_iff. apply Zodd_2p_plus_1. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen