proposition: Lemma full_adder_carry_true : forall a : bool, full_adder_carry a true true = true.
proof: Proof. simple induction a. unfold full_adder_carry in |- *. auto. unfold full_adder_carry in |- *. auto. Qed.
imports: HalfAdder