proposition: Lemma prl_product_can_fun_compat S S' (sd: prl_same_index S S'): prl_map_compat (prl_system_product sd) (prl_product_can_fun S S') ((projective_limit S) \times (projective_limit S')).
proof: Proof. move:(prl_system_product_prop sd) => [ha hb hc hd]. have ssI := prl_same_index_same_I sd. rewrite /prl_product_can_fun ; split; aww. rewrite ha /prl_product_E; move => i iI; rewrite !LgV//. by apply:ext_to_prod_fun_bis; apply:prl_can_fun_fp => //; rewrite - ssI. rewrite hc;move => i j lij; move: (prl_prop0 lij) => [iI jI]; aw. have jI': inc j (psI S') by rewrite - ssI. have lij': gle (psr S') i j by rewrite - sd. move: (ps_function_f lij) (ps_function_f lij'); aw => h3 h4. rewrite hd /prl_product_f !LgV//. rewrite(ext_to_prod_comp_bis (prl_can_fun_fp jI) (prl_can_fun_fp jI') h3 h4). by rewrite - (proj2(prl_can_fun_prop lij)) (proj2(prl_can_fun_prop lij')). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)