proposition: Lemma Eq_powprod a b c: functions a (b \times c) \Eq functions a b \times functions a c.
proof: Proof. move:(two_projections_fb a b c) => h; exists (two_projections a b c). by split => //; rewrite /two_projections; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)