proposition: Lemma highs_is_strip : forall v : BV, highs v = stripbv v 1.
proof: Proof. simple induction v. simpl in |- *. auto with arith. intros. simpl in |- *. rewrite (strip_cons_S bool). rewrite strip_O. trivial with arith. Qed.
imports: BV Adder Gt