proposition: Lemma Exercise1_21cP r u: total_order r -> sub u (substrate r) -> ((forall a b, inc a u -> inc b u -> a = b) <-> ~ (exists x y, glt (induced_order r u) x y)).
proof: Proof. move=> tor usr; split. move => ha hb; move / (Exercise1_21bP tor usr) : hb =>[x [y [xu yu]]]. case; apply (ha _ _ xu yu). move =>h a b au bu; ex_middle ab; case: h. by apply/ (Exercise1_21bP tor usr); exists a, b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)