proposition: Lemma limit_of_continuous_fix x0 x f (seq:= induction_defined f x0) (xn := Lg Nat (Vf seq)): (forall x, realp x -> inc (f x) BR) -> inc x0 BR -> continuous_at f x -> limitR xn x -> realp x -> f x = x.
proof: Proof. move => ha x0r hb hc hd. move: (induction_defined_pr f x0); rewrite -/seq; move => [qa qb qc qd]. have fgx: fgraph xn by rewrite /xn; fprops. have dx: (domain xn) = Nat by rewrite /xn Lgd. have rb: forall n, natp n -> realp (Vg xn n). move => n nN; rewrite /xn LgV//; move: n nN; apply: Nat_induction; first ue. by move => n nN Hr; rewrite qd //; apply: ha. have rc:(forall n : Set, natp n -> realp (f (Vg xn n))). by move => n nN; apply:ha;apply: rb. have ra: BR_seq xn. split => //t /(range_gP fgx) [n nd ->]; apply: rb; rewrite /natp; ue. have rd: realp (f x) by apply: ha. move: (proj2 (limit_of_continuous ra hb hc hd rc rd)). have ->:Lg Nat (fun i => f (Vg xn i)) = Lg Nat (fun i => Vg xn (\1c +c i)). apply:Lg_exten => // i iN; move:(NS_succ iN) => siN. by rewrite csumC - Nsucc_rw // /xn ! LgV//- qd. move => l2; exact: (limitR_unique ra (ha _ hd) hd (limit_of_subset2 l2 NS1) hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)