proposition: Lemma sorted_prop (s: seq R) i j: sorted <%R s -> (i < size s)%N -> (j < size s)%N -> (i < j)%N -> s`_i < s`_j.
proof: Proof. move: i j; elim: s => // a l Hrec i j /= pal; case: i; last first. move => i il; case: j => // j jl /=; rewrite ltnS; apply: Hrec => //. apply: (path_sorted pal). clear Hrec; case: j => // j _ jl _;move: a j jl pal. elim:l => // a l Hrec b j /=;case: j => [_ | j jl]; move /andP => [pa pb] //=. by apply:(lt_trans pa); apply /Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)