proposition: Lemma Exercise1_2b1 r s g r': preorder_quo_axioms r s -> function g -> quotient s = source g -> increasing_pre (g \co (canon_proj s)) r r' -> increasing_pre g (quotient_order r s) r'.
proof: Proof. move=> [_ es sssr] fg qs [pr pr' [fc sq sr'] ale]. split => //. by apply: quotient_is_preorder. by hnf; aw;rewrite substrate_quotient_order//; split => //; rewrite - sr'; aw. have cc: (g \coP (canon_proj s)) by split;fprops; aw; ue. move => x y /quotient_orderP [xq yq h]. have [y0 y0y aux] := (h _ (setQ_repi es xq)). move:(arg1_sr aux)(arg2_sr aux); rewrite - sssr => h2 h1. have h0: source (canon_proj s) = substrate s by aw. move: (ale _ _ aux); rewrite !compfV //; try ue; rewrite !canon_proj_V //. rewrite - (class_eq1 es (related_rep_in_class es yq y0y)). by rewrite (class_rep es xq) (class_rep es yq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)