proposition: Lemma two_projections_aux f a b c: function f -> source f = a -> target f = b \times c -> [/\ lf_axiom (fun z=> P (Vf f z)) a b, lf_axiom (fun z=> Q (Vf f z)) a c, function (first_projection f a b), function (secnd_projection f a c) & (forall x, inc x a -> Vf (first_projection f a b) x = P (Vf f x)) /\ (forall x, inc x a -> Vf (secnd_projection f a c) x = Q (Vf f x))].
proof: Proof. move=> ff sf tf. have ta: lf_axiom (fun z=> P (Vf f z)) a b. rewrite - sf ;move=> t /(Vf_target ff). by rewrite tf; move => /setX_P []. have tb: lf_axiom (fun z=> Q (Vf f z)) a c. rewrite - sf;move=> t /(Vf_target ff). by rewrite tf ; move => /setX_P []. rewrite /first_projection /secnd_projection. by split => //;try (apply: lf_function => //); split; move=> x xa; apply:LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)