proposition: Lemma coarser_gleP x y y': gle (coarser x) y y' <-> [/\ partition_s y x, partition_s y' x & coarser_cs y y'].
proof: Proof. split. by move/Zo_P => [/setXp_P [/partitionsP pa /partitionsP pb]]; aw. move => [pa pb pc]; apply: Zo_i; last by aw. by apply /setXp_P; split;apply /partitionsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)