proposition: Lemma lengthSplit1 : forall {A : Type} (l l' : list A), le (length l) (length l') -> exists p, lengthSplit l l' = Some p.
proof: Proof. induction l as [ | x xs IHxs]. + intros; exists ([], l'); auto. + intros l' LE; destruct l' as [ | b bs] eqn:LEq. - inversion LE. - pose proof IHxs bs as IH; clear IHxs. assert (LE' : le (length xs) (length bs)) by (simpl in *; lia). clear LE. apply IH in LE'; clear IH. inversion LE' as [pair Split]; clear LE'. destruct pair as [l1 l2] eqn:Pair. simpl. rewrite Split. exists (b :: l1, l2). simpl. auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets