proposition: Lemma add_nocarry_mod_lt_pow2 : forall a b n, land a b == 0 -> a mod 2^n + b mod 2^n < 2^n.
proof: Proof. intros a b n H. apply add_nocarry_lt_pow2. - bitwise as m. destruct (le_gt_cases n m). + now rewrite mod_pow2_bits_high. + now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. - apply mod_upper_bound; order_nz. - apply mod_upper_bound; order_nz. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog