proposition: Lemma add_nocarry_lt_pow2 : forall a b n, land a b == 0 -> a < 2^n -> b < 2^n -> a+b < 2^n.
proof: Proof. intros a b n H Ha Hb. rewrite add_nocarry_lxor by trivial. apply div_small_iff. { order_nz. } rewrite <- shiftr_div_pow2, shiftr_lxor, !shiftr_div_pow2. rewrite 2 div_small by trivial. apply lxor_0_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog