proposition: Lemma prl_system_product_prop S S' (sd: prl_same_index S S'): projective_system_on (prl_system_product sd) (prl_product_E S S') (psI S) (psr S) (prl_product_f S S').
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)