proposition: Lemma BV_nat_lem1 : forall (v : BV) (n : nat), lengthbv v <> 0 -> power2 n * BV_to_nat (consbv (lowbit v) nilbv) + power2 (S n) * BV_to_nat (highs v) = power2 n * BV_to_nat v.
proof: Proof. intros. rewrite power2_eq2. rewrite mult_plus_distr_r. replace (BV_to_nat v) with (BV_to_nat (appbv (consbv (lowbit v) nilbv) (highs v))). rewrite BV_to_nat_app2. rewrite (mult_sym (power2 n) (BV_to_nat (consbv (lowbit v) nilbv) + power2 (lengthbv (consbv (lowbit v) nilbv)) * BV_to_nat (highs v))) . rewrite mult_plus_distr_r. simpl in |- *. elim plus_n_O. elim plus_n_O. rewrite mult_plus_distr_r. rewrite (mult_sym (power2 n)). rewrite (mult_sym (power2 n)). trivial with arith. rewrite app_lowbit_highs. trivial with arith. apply (not_nil bool). exact H. Qed.
imports: Definitions