proposition: Lemma length_chunk_base: forall {T: Type} I (x: list T), let i := proj1_sig I in i > 1 -> Datatypes.length x <= i -> Datatypes.length (chunk I x) = 1.
proof: Proof. intros; subst i. funelim (chunk I x). reflexivity. simpl. apply leb_correct in H1. rewrite p in H1. discriminate. Qed.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)