proposition: Lemma Nneq_elim a a' : N.eqb a a' = false -> N.odd a = negb (N.odd a') \/ N.eqb (N.div2 a) (N.div2 a') = false.
proof: Proof. intros. enough (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')) as []. - right. apply Ndiv2_bit_neq; assumption. - left. assumption. - case (N.odd a), (N.odd a'); auto. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits