proposition: Lemma segment_induced r a b: order r -> glt r b a -> segment (induced_order r (segment r a)) b = segment r b.
proof: Proof. move=> or /segmentP ab. exact: (segment_induced_a (segment_segment _ or) ab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)