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