proposition: Lemma seg_order_trans r a b: order r -> glt r a b -> seg_order (seg_order r b) a = seg_order r a.
proof: Proof. move => or ltab; move: (segment_monotone or (proj1 ltab)) => ss. by rewrite /seg_order (segment_induced or ltab) iorder_trans. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)