proposition: Lemma isc_rel_P a b: (related (partition_relation f x) a b <-> in_same_coset f a b).
proof: Proof. move: fpa => [qa qb qc]. split; first by move /graph_on_P1 => [_ _]. by move => h; move: (isc_hi h) => [ax bx]; apply /graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)