proposition: Lemma BV_increment_limit : forall n : nat, BV_increment (list_const bool n true) = list_const bool n false.
proof: Proof. simple induction n. simpl in |- *. auto. intros. simpl in |- *. rewrite H; trivial. Qed.
imports: AdderProof