proposition: Lemma Nodd_not_double a : N.odd a = true -> forall a0, N.eqb (N.double a0) a = false.
proof: Proof. intros H **; eqb2eq. rewrite N.double_spec; intro; subst. rewrite N.odd_mul, N.odd_2 in *; discriminate. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits