proposition: Lemma Exercise1_21f r a b u: total_order r -> sub u (substrate r) -> inc a u -> inc b u -> glt r a b -> without_gaps (induced_order r u) -> without_gaps (induced_order r (u \cap (interval_cc r a b))).
proof: Proof. move=> tor usr au bu ab wg; move: (tor) => [or _]. by apply: Exercise1_21e => //; exists a, b;split => //;apply/setI2_P; split => //;apply /Zo_P;split => //; try split=> //; order_tac; apply: usr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)