proposition: Lemma add_bit1 : forall a b, (a+b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0]).
proof: Proof. intros a b. destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc). simpl in EQ1; rewrite add_0_r in EQ1. rewrite EQ1. autorewrite with bitwise. f_equal. rewrite one_succ, <- div2_bits, EQ2 by order. autorewrite with bitwise. rewrite Hc. simpl. apply orb_false_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog