proposition: Lemma rel_gcp_P x y: inc x (substrate r) -> inc y (quotient r) -> (inc (J x y) (graph (canon_proj r)) <-> inc x y).
proof: Proof. move=> xs yq. have fc: (function (canon_proj r)) by fprops. split => h. move: (Vf_pr fc h). rewrite canon_proj_V //. move => ->; apply/class_P => //; equiv_tac. have: (y = Vf (canon_proj r) x). rewrite (canon_proj_V xs). move: (class_rep er yq) h => <- /(class_P er) rryx. by apply: class_eq1. by move=> ->; Wtac; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)