proposition: Lemma Ndiv2_bit_eq a a' : N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'.
proof: Proof. intros H H'; now rewrite (N.div2_odd a), (N.div2_odd a'), H, H'. Qed.
imports: Bool Sumbool Arith BinPos BinNat Pnat Nnat Ndigits