proposition: Lemma first_proj_fb x y: singletonp y -> bijection (first_proj (x \times y)).
proof: Proof. move=> sy. set f:=first_proj (x \times y). have gp: sgraph (x \times y) by apply: setX_graph. have sp: source f = (x \times y) by rewrite /f/first_proj; aw. have tp: target f = domain(x \times y) by rewrite /f/first_proj; aw. have fp: function (first_proj (x \times y)) by apply: first_proj_f. have [t ty] := sy. split. split=>//; rewrite sp=> a b ap bp. do 2 rewrite first_proj_V =>//. move: ap bp; rewrite ty. move /setX_P=> [ap _] /set1_P pa /setX_P [bp _ /set1_P qb] peq. apply: pair_exten=>//; ue. split => //. rewrite sp tp =>z /(domainP gp) [p px]; ex_tac. by rewrite first_proj_V =>//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)