proposition: Lemma increasing_bounded_limit a xn (x := supremum BR_order (range xn)): BR_seq xn -> (forall n, natp n -> (Vg xn n) <=r a) -> (forall n, natp n -> (Vg xn n) <=r Vg xn (csucc n)) -> (x <=r a /\ limitR xn x).
proof: Proof. move: NS0 => ns0 ha hb hc. set f:= Lg Nat (fun n => BRopp (Vg xn n)). have ar :=(proj32 (hb _ NS0)). set b := BRopp a. have ra: BR_seq f by apply: BR_seq_prop1 => n nN;apply: RSo;apply: BR_seq_prop. have hd: forall n, natp n -> (Vg f n) = BRopp (Vg xn n). move => n nN; rewrite /f LgV//. have rb: (forall n, natp n -> b <=r (Vg f n)). by move => n nN; rewrite (hd _ nN); move:(hb _ nN); move/ rle_opp. have rc: (forall n, natp n -> Vg f (csucc n) <=r Vg f n). by move => n nN; rewrite (hd _ nN) (hd _ (NS_succ nN)); apply/ rle_opp /hc. set y := infimum BR_order (range f). move: (decreasing_bounded_limit ra rb rc);move => [rd re]. have yr: realp y by exact (proj32 rd). have rf: (forall n, natp n -> inc (BRopp (Vg f n)) BR). by move => n / rb [_ fr _]; apply:RSo. move: (ha) => [ha1 ha2 ha3]. have nre: nonempty (range xn). by exists (Vg xn \0c); apply/(range_gP ha1); rewrite ha2; exists \0c. have rbb: (forall t, inc t (range xn) -> t <=r a). by move => t /(range_gP ha1); rewrite ha2; move => [n /hb ww ->]. have rg: xn = (Lg Nat (fun i => BRopp (Vg f i))). rewrite /f;apply:fgraph_exten; fprops; aw;trivial; rewrite ha2 => u uN; rewrite !LgV//. by rewrite (BRopp_K (BR_seq_prop ha uN)). have eq2: (fun_image (range xn) BRopp) = range f. move: ra => [ra1 ra2 ra3]. set_extens t. move =>/funI_P [z /(range_gP ha1) [k kd ->] ->]. apply /(range_gP ra1); rewrite / f; aw; exists k; first ue. rewrite LgV//; ue. move/(range_gP ra1); rewrite ra2; move => [n nN ->]; rewrite /f LgV//. apply /funI_P;exists (Vg xn n)=> //;apply /(range_gP ha1); exists n=> //; ue. move: (proj2(limit_of_continuous ra (continuous_opp yr) re yr rf (RSo yr))). rewrite - (BRopp_K ar). move: (BR_supremum_opp nre rbb); rewrite eq2 - rg -/x -/y => -> h. by split => //; apply:rle_opp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)