proposition: Lemma Neven_not_double_plus_one a : N.even a = true -> forall a0, N.eqb (N.succ_double a0) a = false.
proof: Proof. intros H **; eqb2eq. rewrite N.succ_double_spec; intro; subst. rewrite N.add_comm, N.even_add_mul_2 in *; discriminate. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits