proposition: Lemma full_adder_carry_neg : forall a b : bool, full_adder_carry a (negb a) b = b.
proof: Proof. simple induction a; simple induction b; simpl in |- *. rewrite full_adder_carry_sym1. rewrite full_adder_carry_true. trivial. rewrite full_adder_carry_false. trivial. rewrite full_adder_carry_true. trivial. rewrite full_adder_carry_sym1. rewrite full_adder_carry_false. trivial. Qed.
imports: HalfAdder