proposition: Lemma add_carry_div2 : forall a b (c0:bool), (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0.
proof: Proof. intros a b c0. rewrite <- add3_bits_div2. rewrite (add_comm ((a/2)+_)). rewrite <- div_add by order'. f_equiv. rewrite <- !div2_div, mul_comm, mul_add_distr_l. rewrite (div2_odd a), <- bit0_odd at 1. rewrite (div2_odd b), <- bit0_odd at 1. rewrite add_shuffle1. rewrite <-(add_assoc _ _ c0). apply add_comm. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog