proposition: Lemma Exercise1_21dP r u: total_order r -> sub u (substrate r) -> ((~ without_gaps (induced_order r u)) <-> ((forall a b, inc a u -> inc b u -> a = b) \/ (exists a b, [/\ inc a u, inc b u, glt r a b & (forall z, inc z u -> gle r z a \/ gle r b z)]))).
proof: Proof. move=> tor usr; move: (tor) => [or tor']. move: (iorder_osr or usr) => [oi soi]. rewrite / without_gaps. set P1:= (exists x y, glt (induced_order r u) x y). split => h1. case: (p_or_not_p P1) => np1; [right | left ] =>//; last by apply/(Exercise1_21cP tor usr). ex_middle emh; case: h1; split => //; move=> x y ltxy. ex_middle aux; case: emh. move:(iorder_gle4 ltxy)(iorder_gle2 ltxy)=> [h2 h3] h4. exists x, y; split => //; move => z zu. move: (usr _ zu) (usr _ h2) (usr _ h3) => zs xs ys. case: (tor' _ _ zs ys) => h6; last by right. case: (tor' _ _ xs zs) => h5; last by left. case: (equal_or_not x z) => xz; first by left; rewrite xz; order_tac. case: (equal_or_not y z) => yz; first by right; rewrite yz; order_tac. have zy: z <> y by apply:nesym. case: aux; exists z; apply /iorder_gltP; split => //. move=> [_ P1t h2]. case: h1; first by move /(Exercise1_21cP tor usr); case. move=> [a [b [au bu ab etc]]]. have aux: glt (induced_order r u) a b by apply /iorder_gltP. move: (h2 _ _ aux)=> [z] /iorder_gltP [_ zu za]/iorder_gltP [_ _ zb]. case: (etc _ zu) => h3; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)