proposition: Lemma BV_increment_ok : forall v : BV, BV_to_nat (appbv (BV_increment v) (consbv (BV_increment_carry v) nilbv)) = S (BV_to_nat v).
proof: Proof. intro. rewrite BV_increment_adder. rewrite BV_full_adder_ok. simpl in |- *. elim plus_n_O. elim plus_n_Sm. auto. Qed.
imports: AdderProof