fact: Definition two_projections a b c := Lf (fun z => (J (first_projection z a b) (secnd_projection z a c))) (functions a (b \times c)) ((functions a b) \times (functions a c)).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)