proposition: Lemma full_adder_carry_sym2 : forall a b c : bool, full_adder_carry a b c = full_adder_carry a c b.
proof: Proof. simple induction b. simple induction c. auto. unfold full_adder_carry in |- *. rewrite half_adder_sum_false. rewrite half_adder_carry_false. rewrite half_adder_carry_false. simpl in |- *. elim (half_adder_carry a true); auto. intros. unfold full_adder_carry in |- *. rewrite half_adder_carry_false. rewrite half_adder_sum_false. rewrite half_adder_carry_false. simpl in |- *. elim (half_adder_carry a c); auto. Qed.
imports: HalfAdder