proposition: Lemma limit_of_continuous_fix_pos x0 x f (seq:= induction_defined f x0) (xn := Lg Nat (Vf seq)): (forall x, inc x BRp -> inc (f x) BRp) -> inc x0 BRp -> continuous_at f x -> limitR xn x -> realp x -> f x = x /\ inc x BRp.
proof: Proof. move => pa pb pc pd pe. move:(induction_defined_pr f x0); rewrite -/seq; move => [sa sb sc sd]. have spp: forall i, natp i -> inc (Vf seq i) BRp. by apply: Nat_induction; [ ue | move => n nN Hr; rewrite (sd _ nN); apply:pa]. have ha: forall n, natp n -> \0r <=r Vg xn n. by move => n nN; apply/ rle0xP; rewrite /xn LgV//; apply:spp. have sxn: BR_seq xn by apply: BR_seq_prop1 => n /spp h; apply:BRp_sBR. have xp:inc x BRp by apply/ rle0xP; apply: (limit_positive ha sxn pd pe). have f0r:= (BRp_sBR (pa _ (RpS0))). pose g z := Yo (inc z BRp) (f z) (f \0r). have gp:(forall z, realp z -> realp (g z)). move => z zr; rewrite /g; Ytac h => //; exact (BRp_sBR(pa _ h)). have eq1:(Lg Nat (Vf (induction_defined g x0))) = xn. move:(induction_defined_pr g x0) => [ua ub uc ud]. apply:Lg_exten; apply: Nat_induction; first by rewrite uc sc. by move => n nN h;rewrite (ud _ nN) (sd _ nN) h /g (Y_true (spp _ nN)). have gc: continuous_at g x. move => e ep; move:(pc _ ep) => [d dp dv]; exists d => // y yn. move:(dv _ yn)=>[su sv]; rewrite /BR_near /g (Y_true xp);Ytac h; first done. move: yn => [yr yn]; case/ (BR_i0P): yr => // ym. have oyp:= (BRopp_negative2 (BRms_sBRm ym)). have le1:= (BRsum_Mp pe oyp). suff aa: BR_near x d \0r by exact:(dv _ aa). split; [ apply: RS0| rewrite (BRdiff_0r pe) (BRabs_pos xp) ]. move:yn; rewrite (BRabs_pos (RpS_sum xp oyp)) => le3; exact:(rleT le1 le3 ). move:(limit_of_continuous_fix gp (BRp_sBR pb) gc); rewrite eq1 => hh. by move:(hh pd pe); rewrite /g (Y_true xp) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)