proposition: Lemma addcarryeqn (x y : Z) (c0 : bool) (z := (x + y + Z.b2z c0)) (c := z .^ (x .^ y)) : Z.shiftr c 1 = (x .& y) .| (c .& (x .^ y)).
proof: Proof. case (Z.add_carry_bits x y c0) as (C&?&?&?). enough (Z.shiftr c 1 = (x .& y) .| (c .& (x .| y))) by p. assert (C = (x + y + Z.b2z c0) .^ (x .^ y)) as HC by p. rewrite <-Z.div2_div, Z.div2_spec in H0. subst c z; congruence. Qed.
imports: BinInt Lia Btauto