proposition: Lemma subseq_iota (n m : nat) (l : seq nat) : subseq l (iota n m) = (l == [::]) || (n <= nth 0 l 0)%N && [forall i : 'I_(size l), (nth 0 l i < nth 0 (rcons l (n+m)) i.+1)%N].
proof: Proof. elim:l n m=>[| a l IHl] n m; first by case: (iota n m). elim: m n=>[| m IHm] n. rewrite /addn/addn_rec-plus_n_O. move:(size_iota n 0)=>/size0nil->/=; apply/esym/negbTE. rewrite negb_and orbC -implybE; apply/implyP=>/forallP lmono; rewrite -ltnNge. elim:l a {IHl} lmono=>[| b l IHl] a; first by move=>/(_ 0). by move=>lmono; apply (ltn_trans (lmono 0)); apply IHl=>i/=; apply (lmono (lift ord0 i)). rewrite/iota-/(iota n.+1 m)/subseq. case: ifP. move=>/eqP an; subst a. rewrite -/(subseq l (iota n.+1 m)) (IHl n.+1 m)/= leqnn/=. destruct l=>/=. by apply/esym/forallP; case; case=>//= _; rewrite -{1}(addn0 n) ltn_add2l. apply/andP/forallP. by move=>[nn0 /forallP nl] i; case (ord_S_split i)=>[ [j]->/= | ->// ]; rewrite -addSnnS; apply nl. move=>nl; split; first by apply (nl ord0). by apply/forallP=>i; rewrite addSnnS; apply (nl (lift ord0 i)). move=>an. rewrite -/(subseq (a :: l) (iota n.+1 m)) IHm; congr andb=>/=. by rewrite ltn_neqAle eq_sym an. by rewrite addSnnS. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries