proposition: Lemma gop_V x y: partition_s y x -> Vf (graph_of_partition x) y = partition_relset y x.
proof: Proof. rewrite /graph_of_partition=> pa; rewrite LfV //; first by apply: gop_axioms. by apply /partitionsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)