proposition: Lemma coarser_osr x: order_on (coarser x) (partitions x).
proof: Proof. have sr :substrate (coarser x) = partitions x. apply: extensionality; first by apply: graph_on_sr1. move => t ts. apply: (@arg1_sr _ t t); apply:Zo_i. by apply/setXp_P; split. aw; apply: coarserR. split=> //;split. - by apply: graph_on_graph. - hnf; rewrite sr => y /partitionsP h'. apply/coarser_gleP;split => //; apply: coarserR. - move=> a b c /coarser_gleP [pa _ ab] /coarser_gleP [_ pb bc]. apply /coarser_gleP;split => //; apply: (coarserT ab bc). - move=> a b /coarser_gleP [pa _ ab] /coarser_gleP [pb _ ba]. apply: (coarserA pa pb ab ba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)