proposition: Lemma Exercise1_2c4 r1 r2 f (s := first_proj_eq (substrate r1) (substrate r2)) (r:= order_product2 r1 r2) : function_prop f (quotient s) (substrate r1) -> preorder r1 -> preorder r2 -> ne_substrate r2 -> f \co (canon_proj s)= first_proj (product (substrate r1) (substrate r2)) -> preorder_isomorphism f (quotient_order r s) r1.
proof: Proof. rewrite/function_prop; set (E1:= substrate r1); set (E2:= substrate r2). move=> [ff sf tf] p1 p2 [z zE2] cp. have sr: substrate r = E1 \times E2. by rewrite /r order_product2_sr1. have [es ss] := (first_proj_equivalence E1 E2). have cpa: f \coP (canon_proj s) by saw; apply: canon_proj_f. have pr: preorder r by rewrite /r; apply: order_product2_preorder. have sc: (source (canon_proj s) = E1 \times E2) by aw. have pqa: preorder_quo_axioms r s by split => //; ue. have sq: substrate (quotient_order r s) = source f. by rewrite substrate_quotient_order. have aux: forall x, inc x (source f) -> [/\ inc x (quotient s), inc (rep x) (substrate s) & P (rep x) = Vf f x]. move => x xs. have xqs: inc x (quotient s) by rewrite - sf. have pa: inc (rep x) (substrate s) by fprops. move:(pa) (pa); rewrite ss => pc; rewrite - sc => rsx. split => //; move: (compfV cpa rsx); rewrite cp first_proj_V //. by rewrite canon_proj_V // (class_rep es xqs). have bf: bijection f. split; split => //. move => x y xs ys sW. move:(aux _ xs)(aux _ ys) => [pa b pc] [qa qb qc]. apply /(related_rr_P es pa qa). by apply /first_proj_eq_related_P;split => //; try ue; rewrite pc qc. rewrite tf => y ye1. have Js: (inc (J y z) (source (canon_proj s))) by ue. have ->: (source f = target (canon_proj s)) by aw. exists (Vf (canon_proj s) (J y z)); fprops. by rewrite - (compfV cpa Js) cp first_proj_V //; [ aw| ue]. split => //; [by apply: quotient_is_preorder => //; ue | move=> x y xsf ysf]. move:(aux _ xsf)(aux _ ysf) => [pa b pc] [qa qb qc]. have rx:=(setQ_repi es pa). split. move/quotient_orderP => [_ _ h]. move: (h _ rx) => [w wy /order_product2_P [rpx wp [le1 le2]]]. have yc := (is_class_pr es wy qa). move: (related_rep_class es (inc_in_setQ_sr es wy qa)). by rewrite - yc - pc - qc; move /first_proj_eq_related_P => [_ rys <-]. move=> h; apply/quotient_orderP; split => // w wx. move: (inc_in_setQ_sr es wx pa); rewrite ss => wpr. move/setX_P: (wpr) => [pw Pw Qw]. have JP: (inc (J (Vf f y) (Q w)) ((substrate r1) \times (substrate r2))). apply /setXp_P;split => //; rewrite -/E1 -tf; Wtac. exists (J (Vf f y) (Q w)). rewrite - {2} (class_rep es qa); apply /(class_P es). apply /first_proj_eq_related_P; saw; ue. apply /order_product2_P; saw;split; last by apply: (proj32 p2). have xc:= (is_class_pr es wx pa). move:(related_rep_class es (inc_in_setQ_sr es wx pa)). rewrite -xc; move /first_proj_eq_related_P => [_ _ ->];ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)