proposition: Lemma segment_induced1 r a b: order r -> glt r b a -> segment (induced_order r (segmentc r a)) b = segment r b.
proof: Proof. move=> or /proj1/segmentcP ba. exact: (segment_induced_a (segmentc_segment _ or) ba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)