proposition: Lemma subseq_iota a n b m : b <=a -> a + n <= b + m -> subseq (iota a n) (iota b m).
proof: Proof. move => ba. move: (subnK ba); rewrite addnC => <-; rewrite - addnA leq_add2l => le1. move: (leq_trans (leq_addr n (a-b)) le1) => aux. move: (iotaD b (a-b)(m -(a-b))); rewrite addnC (subnK aux) => ->. rewrite -{1}(cat0s (iota (b + (a - b)) n)); apply: cat_subseq => //. apply: sub0seq. have nm: n <= (m - (a - b)) by rewrite -(leq_add2l (a-b)) subnKC //. set c := (b + (a - b)); move: (iotaD c n ((m - (a - b)) - n)). rewrite addnC (subnK nm) => ->. rewrite -{1}(cats0 (iota c n)); apply: cat_subseq => //; apply: sub0seq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)