proposition: Lemma add_carry_bits : forall a b (c0:bool), exists c, a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0.
proof: Proof. intros a b c0. set (n := max (abs a) (abs b)). apply (add_carry_bits_aux n). - unfold n. destruct (le_ge_cases (abs a) (abs b)); [rewrite max_r|rewrite max_l]; order_pos'. - assert (Ha : abs a < 2^n). + apply lt_le_trans with (2^(abs a)). * apply pow_gt_lin_r; order_pos'. * apply pow_le_mono_r. { order'. } unfold n. destruct (le_ge_cases (abs a) (abs b)); [rewrite max_r|rewrite max_l]; try order. + apply abs_lt in Ha. destruct Ha; split; order. - assert (Hb : abs b < 2^n). { apply lt_le_trans with (2^(abs b)). - apply pow_gt_lin_r; order_pos'. - apply pow_le_mono_r. { order'. } unfold n. destruct (le_ge_cases (abs a) (abs b)); [rewrite max_r|rewrite max_l]; try order. } apply abs_lt in Hb. destruct Hb; split; order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog