proposition: Lemma gop_axioms x: lf_axiom (fun y => partition_relset y x) (partitions x) (\Po (coarse x)).
proof: Proof. by move=> y /partitionsP => h; apply/setP_P /sub_part_relsetX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)