proposition: Lemma Exercise1_2e5 r: total_order r -> finite_set (substrate r) -> \3c <=c cardinal (substrate r) -> exists s, [/\ equivalence s, substrate s = substrate r, total_order (quotient_order r s), ~ ( weak_order_compatibility r s) & ~ ( Ex1_2_hC' r s) ].
proof: Proof. move => tor fso /(Exercise1_2e4 tor) [a [b [c [ab bc]]]]. move: (Exercise1_2e2 (proj1 tor) ab bc). set s := _\cup _; move => [es ss pa pb]; exists s;split => //. by apply: Exercise1_2e1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)