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