proposition: Lemma prl_exa3_prop6 x: inc x (projective_limit prl_exa3_system) -> (natp (Vg x \0c) /\ forall i, natp i -> Vg x \0c = (Vg x i) +c i).
proof: Proof. move=> /prl_limitP /= [ha hb hc hd]. have ns0 := NS0. have rd: inc (Vg x \0c) Nat by move:(hc _ NS0); rewrite /Efam LgV. split => // i iN. have le1: gle r \0c i. by apply/(proj33 prl_exa3_prop1);split; fprops; apply:cle0n. have ra: inc (Vg x i) Nat by move:(hc _ iN); rewrite /Efam LgV. have rb:= (prl_exa3_prop3 le1). move:(hd _ _ le1); rewrite /ffam /f LgV// LfV//; aw;trivial. rewrite (cdiff_n0 iN). move:(hd _ _ le1); rewrite /ffam /f LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)