proposition: Theorem half_adder_ok : forall a b : bool, bool_to_nat (half_adder_sum a b) + (bool_to_nat (half_adder_carry a b) + bool_to_nat (half_adder_carry a b)) = bool_to_nat a + bool_to_nat b.
proof: Proof. simple induction a; simple induction b; auto. Qed.
imports: Arith_compl Bool_compl