proposition: Lemma seq2_ind (P : seq T1 -> seq T2 -> Prop) : P [::] [::] -> (forall x1 x2 s1 s2, P s1 s2 -> P (x1 :: s1) (x2 :: s2)) -> forall s1 s2, size s1 = size s2 -> P s1 s2.
proof: Proof. move=> Pnil Pcons. elim=> [|x1 l1 IH1]; case=> // x2 l2 /eqnP /= Hs. by apply/Pcons/IH1/eqnP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)