proposition: Lemma prl_r3_res0 i (H: inc i prl_r3_nI): prl_r3_Fl i = (projective_limit (prl_restr (prl_r3_prop4 H))).
proof: Proof. by rewrite /prl_r3_Fl /prl_r3_systemi;case: (ixm (inc i prl_r3_nI)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)