proposition: Lemma BV_full_adder_nil_ok : forall (v : BV) (cin : bool), BV_to_nat (BV_full_adder v nilbv cin) = BV_to_nat v + bool_to_nat cin.
proof: Proof. simple induction v. simple induction cin; auto with arith. simple induction cin. rewrite BV_full_adder_nil_true_ok. simpl in |- *. auto with arith. unfold BV_full_adder in |- *. rewrite BV_full_adder_sum_v_nil_false. rewrite BV_full_adder_carry_v_nil_false. rewrite BV_to_nat_app2. simpl in |- *. elim mult_n_O. elim plus_n_O. trivial with arith. Qed.
imports: Adder