proposition: Lemma prl_dl3_mod_p1 x: inc x (projective_limit prl_dl3_systemS) -> inc (prl_dl3_mod x) (productb (Lg I prl_dl3_Ep)).
proof: Proof. move => /prl_limitP /= [p1 p2 p3 _]. rewrite /prl_dl3_mod; apply/setXb_P;aw; split; fprops => i iI; rewrite !LgV//. apply/setXb_P; rewrite /prl_dl3_Efam; aw; split; fprops => j jL; rewrite !LgV//. have pp: inc (J i j) (I \times L) by apply: setXp_i. by move: (p3 _ pp);rewrite /prl_dl3_E LgV//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)