proposition: Theorem full_adder_ok : forall a b c : bool, bool_to_nat (full_adder_sum a b c) + (bool_to_nat (full_adder_carry a b c) + bool_to_nat (full_adder_carry a b c)) = bool_to_nat a + bool_to_nat b + bool_to_nat c.
proof: Proof. simple induction a; simple induction b; simple induction c; auto. Qed.
imports: HalfAdder