proposition: Lemma subseq_iota1 i m: i<m -> subseq ([:: i; i.+1]) (iota 0 m.+1).
proof: Proof. have ->: [:: i; i.+1] = iota i 2 by []. by move => im; apply: subseq_iota => //; rewrite add0n addn2 ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)