proposition: Lemma Exercise1_2e4 r: total_order r -> \3c <=c cardinal (substrate r) -> exists a b c, glt r a b /\ glt r b c.
proof: Proof. move => [or tor] /cardinal_ge3; rewrite /glt. move => [a [b [c [ae be ce [ab bc ac]]]]]. case:(tor _ _ ae be) => h1; case: (tor _ _ be ce) => h2; first by exists a,b,c. case: (tor _ _ ae ce) => h3; [ exists a,c, b | exists c, a,b ]; fprops. case: (tor _ _ ae ce) => h3; [ exists b,a,c | exists b,c, a]; fprops. exists c, b, a; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)