proposition: Lemma length_chunk_lt: forall {T: Type} I (x: list T), let i := proj1_sig I in i > 1 -> Datatypes.length x > i -> Datatypes.length (chunk I x) < Datatypes.length x.
proof: Proof. intros; subst i. funelim (chunk I x). simpl. lia. simpl. specialize (H H0). revert H. unfold drop. simpl. pose proof (drop_spec (` i) x). simpl in H. rewrite H by lia. clear H. simp chunk. clear Heq. destruct dec. simp chunk; simpl; intros; try lia. intros. feed H. clear H. apply leb_complete_conv in e. pose proof (drop_spec (` i) x). rewrite H in e; try lia; unfold length in *; simpl in *; lia. lia. Qed.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)