proposition: Lemma two_projections_fb a b c: bijection (two_projections a b c).
proof: Proof. move: (@two_projections_ax a b c) => ta. rewrite /two_projections; apply: lf_bijective => //. move=> u v /functionsP [fu su tu] /functionsP [fv sv tv] h. move: (pr1_def h)(pr2_def h) => sfp ssp. apply: function_exten=> //; try ue;rewrite su. move=> x xa. move: (two_projections_aux fu su tu) (two_projections_aux fv sv tv). move=> [h1 h2 h3 h4 [h5 h6]][h7 h8 h9 h10 [h11 h12]]. have /setX_P [<- _ _]: (inc (Vf u x)(b \times c)) by rewrite -tu; Wtac. have /setX_P [<- _ _] : (inc (Vf v x)(b \times c)) by rewrite -tv; Wtac. rewrite -(h5 _ xa) - (h11 _ xa) sfp -(h6 _ xa) - (h12 _ xa) ssp //. move=> y /setX_P [yp] /functionsP [fp sp tp] /functionsP [fq sq tq]. set (f:= Lf (fun z=> J (Vf (P y) z) (Vf (Q y) z)) a (b \times c)). have tb: (lf_axiom (fun z=> J (Vf (P y) z) (Vf (Q y) z)) a (b \times c)). move=> z za; apply /setXp_i; [rewrite -tp|rewrite -tq]; Wtac. have ff:(function f) by apply: lf_function. have sf: (source f = a) by rewrite /f; aw. have tf: (target f = b \times c) by rewrite /f; aw. move: (two_projections_aux ff sf tf) => [h1 h2 h3 h4 [h5 h6]]. exists f => //; first by apply /functionsP. by rewrite - yp; congr J; apply: function_exten; rewrite / first_projection /secnd_projection; aw; trivial; [rewrite sp | rewrite sq ]; move=> x xsr /=; rewrite LfV // /f LfV //; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)