proposition: Lemma Nnot_div2_not_double_plus_one a a0 : N.eqb (N.div2 a) a0 = false -> N.eqb (N.succ_double a0) a = false.
proof: Proof. intros H. eqb2eq. contradict H. subst. apply N.div2_succ_double. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits