proposition: Lemma lengthSplit2 : forall {A : Type} (l l' l1 l2 : list A), lengthSplit l l' = Some (l1, l2) -> l1 ++ l2 = l'.
proof: Proof. induction l. + intros l' l1 l2 Hyp; simpl in Hyp; inversion_clear Hyp; auto. + intros l' l1 l2 Hyp. simpl in Hyp. destruct l' as [ | y ys] eqn:L'. - inversion Hyp. - destruct l1 eqn:L1. * destruct (lengthSplit l ys); simpl in *. + destruct p; congruence. + congruence. * pose proof IHl ys l0 l2; clear IHl. destruct (lengthSplit l ys) eqn:LenSplit; simpl in *. + inversion Hyp. destruct p. inversion H1. subst. rewrite H; auto. + inversion Hyp. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets