proposition: Lemma full_adder_sum_sym2 : forall a b c : bool, full_adder_sum a b c = full_adder_sum a c b.
proof: Proof. simple induction b. simple induction c. auto. unfold full_adder_sum in |- *. rewrite half_adder_sum_false. rewrite half_adder_sum_false. auto. unfold full_adder_sum in |- *. rewrite half_adder_sum_false. intro. auto. Qed.
imports: HalfAdder