proposition: Lemma bv_extr_size: forall (i n0 n1 : N) a, size a = n1 -> size (@bv_extr i n0 n1 a) = n0%N.
proof: Proof. intros. unfold bv_extr, size in *. case_eq (n1 <? n0 + i)%N. intros. now rewrite length_mk_list_false, N2Nat.id. intros. specialize (@length_extract a i (n0 + i)). intros. assert ((n0 + i - i) = n0)%N. { lia. } rewrite H2 in H1. rewrite H1. now rewrite N2Nat.id. rewrite H. now apply not_ltb. lia. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance