proposition: Lemma _length_extract: forall a (i j: N) (H0: (N.of_nat (length a)) >= j) (H1: j >= i), length (extract a 0 (N.to_nat j)) = (N.to_nat j).
proof: Proof. intro a. induction a as [ | xa xsa IHa ]. - simpl. case i in *. case j in *. easy. lia. case j in *; lia. - intros. simpl. case_eq j. intros. now simpl. intros. rewrite <- H. case_eq (N.to_nat j). easy. intros. simpl. apply f_equal. specialize (@IHa 0%N (N.of_nat n)). rewrite Nat2N.id in IHa. apply IHa. apply (f_equal (N.of_nat)) in H2. rewrite N2Nat.id in H2. rewrite H2 in H0. simpl in *. lia. lia. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance