proposition: Lemma subseq_incl (T: eqType) (s s': seq T) x: subseq s s' -> {f: 'I_(size s) -> 'I_(size s') | (forall i, nth x s' (f i) = nth x s i) /\ {homo f : y x / (x < y)%O >-> (x < y)%O}}.
proof: Proof. elim: s' s=> [| a s' IHs'] s sub. by move:sub=>/eqP -> /=; exists id; split=>// i j. case: s sub=> [ _ | b s sub]. move=>/=; simple refine (exist _ _ _). by move=> i; case: i. by split; move=> i; case: i. move: sub=>/=; case sa: (b == a). move: sa=>/eqP <- /IHs' [f [fn flt]]. exists (fun i => match ord_S_split i with | inleft j => lift ord0 (f (proj1_sig j)) | inright _ => ord0 end). split. by move=> i; case: ord_S_split=> [ [j ie] | ie ]; subst i=>/=. move=> i j; case: ord_S_split=> [ [i' ie] | ie ]; case: ord_S_split=> [ [j' je] | je ]; subst i j=>//=. do 2 rewrite ltEord=>/=. by rewrite /bump /= add1n add1n add1n add1n ltnS ltnS; apply flt. by move=>/IHs' [f [fn flt]]; exists (fun i => lift ord0 (f i)). Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)