proposition: Lemma Exercise1_21e r u a b: total_order r -> let v:= u \cap (interval_cc r a b) in sub u (substrate r) -> without_gaps (induced_order r u) -> (exists x y, [/\ inc x v, inc y v & glt r x y]) -> without_gaps (induced_order r v).
proof: Proof. move=> tor v usr wg h1. have svu: (sub v u) by apply: subsetI2l. have svi: (sub v (interval_cc r a b)) by apply: subsetI2r. have svr: (sub v (substrate r)) by apply: (sub_trans svu). ex_middle wg1. move: wg1 => /(Exercise1_21dP tor svr) wg1. have: (~ ~ without_gaps (induced_order r u)) by case. move /(Exercise1_21dP tor usr) => wg2. case: wg2; case: wg1. by move:h1 => [c [d [cv dv [_ cd]]]] h2; move: (h2 _ _ cv dv). move=> [c [d [cv dv cd icd]]]; right; exists c; exists d; split;fprops. move=> z szu. move: tor => [or tor]. case: (tor _ _ (usr _ szu) (svr _ cv)) => zc; first by left. case: (tor _ _ (svr _ dv) (usr _ szu) ) => zd; first by right. move: cv dv => /setI2_P [_] /Zo_hi [ac _] /setI2_P [_] /Zo_hi [_ db]. apply: icd; apply: setI2_i => //; apply: Zo_i ; [| split => //]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)