proposition: Lemma decreasing_limit_bounded_fix a x0 f (seq:= induction_defined f x0) (xn := Lg Nat (Vf seq)) (x := infimum BR_order (range xn)): (forall x, a <=r x -> a <=r f x /\ f x <=r x) -> a <=r x0 -> (continuous_at f x) -> [/\ a <=r x, f x = x & limitR xn x].
proof: Proof. move => fp x0p fc. move: (proj31 x0p) => ar. move:(induction_defined_pr f x0) => []; rewrite -/seq => ua ub uc ud. have ha: forall n, natp n -> a <=r (Vf seq n). apply: Nat_induction. ue. move => n nN H; rewrite (ud _ nN). exact:(proj1 (fp _ H)). have hb: (forall n, natp n -> a <=r (Vg xn n)). by move => n nN; rewrite /xn LgV//; apply: ha. have hc: BR_seq xn by apply:BR_seq_prop1 => n /ha []. have hd: (forall n, natp n -> Vg xn (csucc n) <=r Vg xn n). move => n nN; move: (NS_succ nN) => snN;rewrite /xn !LgV// (ud _ nN). exact (proj2(fp _ (ha _ nN))). have fp1: forall x, a <=r x -> a <=r f x by move => t /fp []. move:(decreasing_bounded_limit hc hb hd) => [he hf]. move: (limit_of_continuous_fix_gea ar fp1 x0p fc hf (proj32 he)). by move => [sa sb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)