proposition: Lemma BV_to_nat_lem0 : forall v : BV, lengthbv v <> 0 -> BV_to_nat v = BV_to_nat (consbv (lowbit v) nilbv) + power2 1 * BV_to_nat (highs v).
proof: Proof. intros. rewrite lowbit_is_trunc. rewrite highs_is_strip. replace (power2 1) with (power2 (length (trunc bool v 1))). rewrite <- BV_to_nat_app2. rewrite (app_trunc_strip bool). trivial with arith. rewrite (length_trunc bool). trivial with arith. apply (le_SO_length_v bool). exact H. apply (not_nil bool). exact H. Qed.
imports: Definitions