proposition: Lemma limit_of_continuous_fix_gea a x0 x f (seq:= induction_defined f x0) (xn := Lg Nat (Vf seq)): realp a -> (forall x, a <=r x -> a <=r (f x)) -> a <=r x0 -> continuous_at f x -> limitR xn x -> realp x -> f x = x /\ a <=r x.
proof: Proof. move => h0 h1 h2 h3 h4 h5. have eq0 := (BRsum_diff h0 h5). have fxr :=(continuous_real h5 h3). pose g x := f (a +r x) -r a. set yn := Lg Nat (Vf (induction_defined g (x0 -r a))). have eq1: (f x) -r a = g (x -r a) by rewrite /g eq0. have k1:(forall t, inc t BRp -> inc (g t) BRp). move => t tp; move:(h1 _ (BRsum_Mp h0 tp)) => ra. by apply/(rle_diffP h0 (proj32 ra)). have k2: inc (x0 -r a) BRp by apply/ (rle_diffP h0 (proj32 h2)). have k3: continuous_at g (x -r a). rewrite - eq0 in h3 fxr. have ra := (proj1 (continuous2_sum h0 (RS_diff h5 h0))). have rb :=(proj2 (continuous2_diff fxr h0)). exact:(continuous_comp ra (continuous_comp h3 rb)). have k4: limitR yn (x -r a). have rb :=(proj2 (continuous2_diff h5 h0)). move: (induction_defined_pr f x0) => []; rewrite -/seq => sa sb sc sd. move: (induction_defined_pr g (x0 -r a)) => [sa' sb' sc' sd']. have a0: forall n, natp n -> a <=r (Vf seq n). apply:Nat_induction; [ue | by move => n nN; rewrite (sd _ nN); apply: h1]. have a1: forall n, natp n -> realp (Vf seq n) by move => n /a0 []. have a2: BR_seq xn by apply: BR_seq_prop1 => n /a1. have a3: forall n, natp n -> realp (Vg xn n -r a). move => n nN; rewrite /xn LgV//;apply: RS_diff => //; fprops. have ns0 := NS0. move:(proj2 (limit_of_continuous a2 rb h4 h5 a3 (RS_diff h5 h0))). congr(limitR _ (x -r a)); rewrite /xn/seq;apply: Lg_exten. apply: Nat_induction; first by rewrite LgV // sc sc'. move => n nN;move: (NS_succ nN) => snN; rewrite !LgV// => H. rewrite (sd _ nN) (sd' _ nN) - H /g BRsum_diff; fprops. have k5: inc (x -r a) BR by apply: RS_diff. move:(limit_of_continuous_fix_pos k1 k2 k3 k4 k5). rewrite /g (BRsum_diff h0 h5); move => [/(BRsum_eq2r fxr h5 (RSo h0)) ra]. by move /(rle_diffP h0 h5) => rb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)