proposition: Lemma first_proj_eq_related_P x y a b: related (first_proj_eq x y) a b <-> [/\ inc a (x \times y), inc b (x \times y) & P a = P b].
proof: Proof. have ff: function (first_proj (x \times y)) by apply:first_proj_f. split. move/(ea_relatedP ff); rewrite lf_source; move => [pa pb]. by rewrite ! first_proj_V. by move => [pa pb pc]; apply/(ea_relatedP ff);rewrite lf_source !first_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)