proposition: Theorem segments_iso_is r: worder r -> order_isomorphism (segments_iso r) r (sub_order (segmentss r)).
proof: Proof. move=> wor;move: (wor)=> [or worp]. have ta: lf_axiom (segment r) (substrate r) (segmentss r). by move => t ts; apply /funI_P; ex_tac. move: (sub_osr (segmentss r)) => [pa pb]. hnf; rewrite /segments_iso;split => //. split;aw => //; apply: lf_bijective=> //. + move=> u v; apply: (segment_injective (worder_total wor)). + move=> y /funI_P [z za ->];ex_tac. hnf; aw;move=> x y xsr ysr; rewrite !LfV //; split. move=> hyp; apply/sub_gleP;split => //; fprops. by apply: segment_monotone. move /sub_gleP=> [_ _ ss]. exact: (segment_monotone1 (worder_total wor) xsr ysr ss). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)