proposition: Lemma BV_to_nat_app : forall (l n : BV) (ll : nat), lenbv l ll -> BV_to_nat (appbv l n) = BV_to_nat l + power2 ll * BV_to_nat n.
proof: Proof. unfold BV, lenbv, appbv in |- *. simple induction l. intros. inversion H. simpl in |- *. auto. intros. simpl in |- *. inversion H0. simpl in |- *. rewrite (H n l1). rewrite mult_plus_distr_r. repeat rewrite plus_assoc. rewrite (plus_permute2 (bool_to_nat a + BV_to_nat l0) (power2 l1 * BV_to_nat n) (BV_to_nat l0)). auto. exact H4. Qed.
imports: Arith_compl Bool_compl Lists_replace