proposition: Lemma Exercise1_4b r: order r -> total_order(quotient_order r (ncr_equiv r)).
proof: Proof. move => or. move: (ncr_properties or) => [p1 p2 p3 p4]. have sa:(substrate (quotient_order r (ncr_equiv r)) = quotient (ncr_equiv r)). rewrite substrate_quotient_order /preorder_quo_axioms; split => //. by apply order_preorder. have oq:(order (quotient_order r (ncr_equiv r))). apply: Exercise1_2d => // x y z xy yz xz. case: (p_or_not_p (related (ncr_equiv r) x y)) => // nxy. have yy: (related (ncr_equiv r) y y). by apply: reflexivity_e =>//; rewrite p2; order_tac. have nsc:(class (ncr_equiv r) x <> class (ncr_equiv r) y). dneg sc; apply: symmetricity_e =>//; apply /(related_equiv_P p1);split => //; rewrite p2; order_tac. move: (Exercise1_4b1 or xz yy nsc xy) => zy. rewrite (order_antisymmetry or yz zy) //. split => //. rewrite sa => x y xq yq. case: (equal_or_not x y) => nxy; first by rewrite nxy; left; order_tac; ue. move:(setQ_repi p1 xq) (setQ_repi p1 yq) => rx ry. have rxs: (inc (rep x) (substrate r)) by rewrite -p2; apply: rep_i_sr. have rys: (inc (rep y) (substrate r)) by rewrite -p2; apply: rep_i_sr. have nsc:class (ncr_equiv r) (rep x) <> class (ncr_equiv r) (rep y). by dneg bad; move: xq yq => /(setQ_P p1) [_ -> ] /(setQ_P p1) [_ -> ]. case: (Exercise1_4a1 or rxs rys); last by done. move:(related_rep_in_class p1) => H. case => cv; [left | right]; apply /quotient_orderP; split => //. move=> u ux; exists (rep y) => //. exact: (Exercise1_4b1 or (H _ _ xq ux) (H _ _ yq ry) nsc cv). move=> u ux; exists (rep x) => //. exact: (Exercise1_4b1 or (H _ _ yq ux) (H _ _ xq rx) (nesym nsc) cv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)