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. destruct (le_gt_cases a 0) as [Ha'|Ha']. - apply le_lt_trans with (0+b). + now apply add_le_mono_r. + now nzsimpl. - destruct (le_gt_cases b 0) as [Hb'|Hb']. + apply le_lt_trans with (a+0). * now apply add_le_mono_l. * now nzsimpl. + rewrite add_nocarry_lxor by order. destruct (lt_ge_cases 0 (lxor a b)); [|apply le_lt_trans with 0; order_pos]. apply log2_lt_pow2; trivial. apply log2_lt_pow2 in Ha; trivial. apply log2_lt_pow2 in Hb; trivial. apply le_lt_trans with (max (log2 a) (log2 b)). * apply log2_lxor; order. * destruct (le_ge_cases (log2 a) (log2 b)); [rewrite max_r|rewrite max_l]; order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog