proposition: Lemma related_e_P u v: related r u v <-> [/\ inc u (source (canon_proj r)), inc v (source (canon_proj r)) & Vf (canon_proj r) u = Vf (canon_proj r) v].
proof: Proof. rewrite canon_proj_s; split. by move/(related_equiv_P er)=> [us vs cuv]; split=> //; rewrite !canon_proj_V. move => [us vs h]; apply/(related_equiv_P er); split => //; move: h. by rewrite !canon_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)