proposition: Lemma Exercise1_2e1 r s: equivalence s -> total_order r -> substrate s = substrate r -> finite_set (substrate r) -> total_order (quotient_order r s).
proof: Proof. move => eqs tor ssr fs. have or := (proj1 tor). have pr := (order_preorder or). have [p1 p2 p3] := (quotient_is_preorder (And3 pr eqs ssr)). pose gr x := (the_greatest (induced_order r x)). pose A x := (inc (gr x) x /\ forall y, inc y x -> gle r y (gr x)). have gp: forall x, sub x (substrate r) -> nonempty x -> A x. move => x xsr nex. have h := (finite_subset_torder_greatest tor (sub_finite_set xsr fs) nex xsr). have [pa' pb'] := (iorder_osr or xsr). case: (the_greatest_pr pa' h); rewrite -/ (gr x) pb' => pa pb. split => // y yx; exact: (iorder_gle1 (pb _ yx)). have gp1: forall x, inc x (quotient s) -> A x. move => x xq; apply: gp (setQ_ne eqs xq). move => t tx; rewrite - ssr; apply: (inc_in_setQ_sr eqs tx xq). have paP: forall x y, related (quotient_order r s) x y <-> [/\ inc x (quotient s),inc y (quotient s) & gle r (gr x) (gr y)]. move => x y; apply: (iff_trans (quotient_orderP r s x y)). split; move=> [pa pb pc];move: (gp1 _ pa) (gp1 _ pb)=> [qa qb][qc qd]. split => //; move: (pc _ qa) => [z /qd le2 le1]; order_tac. split => //t tx; ex_tac; move: (qb _ tx) => le1; order_tac. split. split => // x y /paP [xq yq le1] /paP [_ _ le2]. have sv: (gr x) = (gr y) by order_tac. move: (gp1 _ xq) (gp1 _ yq) => [xs _] [ys _]. by rewrite (is_class_pr eqs xs xq) (is_class_pr eqs ys yq) sv. rewrite (substrate_quotient_order (And3 pr eqs ssr)) => x y xsr ysr. move: (proj1 (gp1 _ xsr)) (proj1 (gp1 _ ysr)) => xs ys. move: (inc_in_setQ_sr eqs xs xsr); rewrite ssr => x1. move: (inc_in_setQ_sr eqs ys ysr); rewrite ssr => y1. by case: (proj2 tor _ _ x1 y1) =>h; [left | right]; apply /paP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)