proposition: Lemma BV_full_adder_carry_v_nil_false : forall v : BV, BV_full_adder_carry v nilbv false = false.
proof: Proof. unfold nilbv in |- *. simple induction v. trivial. intros. rewrite BV_full_adder_carry_eq3. rewrite half_adder_carry_false. trivial. Qed.
imports: BV FullAdder