proposition: Lemma lengthSplit3 : forall {A : Type} (l l' l1 l2 : list A), lengthSplit l l' = Some (l1, l2) -> length l1 = length l.
proof: Proof. induction l as [ | x xs IHxs]. + intros; simpl in H; inversion H; auto. + intros l' l1 l2 Split. simpl in Split. destruct l'. - inversion Split. - destruct l1. * destruct (lengthSplit xs l'). + simpl in *. destruct p. inversion Split. + simpl in *. inversion Split. * simpl in *. destruct (lengthSplit xs l') eqn:LenSplit. + simpl in *. destruct p. inversion Split; subst; clear Split. pose proof (IHxs l' l1 l2 LenSplit) as Hyp; clear IHxs. auto. + simpl in *. inversion Split. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets