proposition: Lemma first_proj_equiv_proj x y: nonempty y-> bijection (Lf (fun u => (singleton u) \times y) x (quotient (first_proj_eq x y))).
proof: Proof. move=> ney. set (f:=fun u => (singleton u) \times y). set (g:= (Lf f x (quotient (first_proj_eq x y)))). have efp:=(proj1 (first_proj_equivalence x y)). have ta: lf_axiom f x (quotient (first_proj_eq x y)). move => u ux ; apply /(setQ_P efp) /(first_proj_classP _ ney); ex_tac. rewrite /g; apply: lf_bijective => //. rewrite /f => u v ux vx sp. apply: set1_inj; rewrite - (setX_domain (singleton u) ney). by rewrite sp setX_domain. move=>z /(setQ_P efp) /(first_proj_classP _ ney) [u ux ep]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)