proposition: Lemma length_BV_decrement : forall v : BV, lengthbv (BV_decrement v) = lengthbv v.
proof: Proof. simple induction v. auto. simple induction a. simpl in |- *. intros. trivial. simpl in |- *. intros. rewrite H; trivial. Qed.
imports: AdderProof