proposition: Lemma first_proj_equivalence x y: equivalence_on (first_proj_eq x y) (x \times y).
proof: Proof. by move:(graph_ea_equivalence (first_proj_f (x\times y))); rewrite lf_source. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)