proposition: Lemma size_ind (A:Type) (P: seq A -> Prop): (forall l, (forall s, size s < size l -> P s) -> P l) -> (forall l, P l).
proof: Proof. move => hb l; move:{2} (size l) (leqnn (size l)) => n; elim: n l. by move=> l h; apply:hb => s ss; move: (leq_trans ss h); rewrite ltn0. move => n Hr l; rewrite leq_eqVlt => /orP; case => kp2; last by apply: Hr. by apply: hb =>s; rewrite (eqP kp2) ltnS; apply: Hr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)