proposition: Lemma gop_morphism x: order_morphism (graph_of_partition x) (coarser x) (opp_order (subp_order (coarse x))).
proof: Proof. have [oi sr] := (sub_osr (coarse x)). have [oc sr'] := (coarser_osr x). have [pa1 pb1] := (subp_osr (coarse x)). have [pa2 pb2] := (opp_osr pa1). have gi: (sgraph (sub_order (coarse x))) by fprops. have sg: source (graph_of_partition x) = (partitions x). by rewrite /graph_of_partition; aw. split;fprops. split; rewrite ? pb2 ? pb1 ? sr' /graph_of_partition;aw; trivial. by apply: lf_function; apply: gop_axioms. hnf;rewrite sg => a b /partitionsP pa /partitionsP pb. rewrite - partition_relset_order // gop_V // gop_V //. split; last by move/igraph_pP => /sub_gleP [_ _]. move => h; apply/igraph_pP; apply /sub_gleP. by split => //; apply /setP_P /sub_part_relsetX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)