proposition: Lemma add_nocarry_lxor : forall a b, land a b == 0 -> a+b == lxor a b.
proof: Proof. intros a b H. destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc). simpl in EQ1; rewrite add_0_r in EQ1. rewrite EQ1. apply (nocarry_equiv a b c) in H; trivial. rewrite H. now rewrite lxor_0_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog