proposition: Lemma add_nocarry_mod_lt_pow2 : forall a b n, 0<=n -> land a b == 0 -> a mod 2^n + b mod 2^n < 2^n.
proof: Proof. intros a b n Hn H. apply add_nocarry_lt_pow2. - bitwise as m ?. destruct (le_gt_cases n m). + rewrite mod_pow2_bits_high; now split. + now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. - apply mod_pos_bound; order_pos. - apply mod_pos_bound; order_pos. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog