proposition: Lemma prl_restr_canonical_comp S K K' (H1:sub K (psI S)) (H2: sub K' K) (g := prl_restr_canonical H1) (g' := prl_restr_canonical (H2: sub K' (psI (prl_restr H1)))) (g'' := prl_restr_canonical (sub_trans H2 H1)): g' \coP g /\ g' \co g = g''.
proof: Proof. case: (prl_restr_canonical_fp H1) => [pa pb pc]. case: (prl_restr_canonical_fp (sub_trans H2 H1))=> [pa'' pb'' pc'']. case:(prl_restr_canonical_fp (H2: sub K' (psI (prl_restr H1))))=> [pa' pb' pc']. have hu: g' \coP g by hnf; rewrite pc pb'. split => //; apply: (function_exten (compf_f hu) pa''); aw. - by rewrite pb pb''. - by rewrite pc'' pc' (projective_limit_restr_double H1 H2). - move => t tg /=; move:(tg); rewrite pb => tg'. rewrite /g/g' compfV // !prl_restr_canonical_fun_ev //. by rewrite double_restr. exact: (prl_restr_canonical_ax H1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)