proposition: Lemma length_highs : forall v : BV, v <> nilbv -> lengthbv (highs v) = pred (lengthbv v).
proof: Proof. intros. rewrite highs_is_strip. rewrite (length_strip bool). apply minus_n_SO. apply (v_not_nil_length bool). exact H. Qed.
imports: BV Adder Gt