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