proposition: Lemma Exercise1_21bP r u: total_order r -> sub u (substrate r) -> ((exists x y, glt (induced_order r u) x y) <-> (exists x y, [/\ inc x u, inc y u & x<> y])).
proof: Proof. move=> [or tor] uv; split. move=> [x [y [h1 h2]]]. move: (iorder_gle3 h1) => [xr yr]; exists x, y; split => //. move=> [x [y [h1 h3 h4]]]; case: (tor _ _ (uv _ h1) (uv _ h3)) => h5. by exists x; exists y; split =>//; apply /iorder_gleP. by exists y; exists x; split; [ apply /iorder_gleP |apply:nesym ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)