proposition: Lemma hom_lt_inj {disp disp' : unit} {T : orderType disp} {T' : porderType disp'} [f : T -> T'] : {homo f : x y / (x < y)%O >-> (x < y)%O} -> injective f.
proof: Proof. move=>flt i j. move: (Order.TotalTheory.le_total i j). wlog: i j / (i <= j)%O. move=>h /orP; case=>le fij. by apply (h i j)=>//; rewrite le. by apply/esym; apply (h j i)=>//; rewrite le. rewrite Order.POrderTheory.le_eqVlt=>/orP; case=> [ /eqP ij | /flt fij ]=>// _ fije. by move: fij; rewrite fije Order.POrderTheory.lt_irreflexive. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)