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