proposition: Lemma continuous_prod f g x: realp x -> continuous_at f x -> continuous_at g x -> continuous_at (fun z => f z *r g z) x.
proof: Proof. move => xr pa pb. move:(continuous_real xr pa) (continuous_real xr pb) => fxr gxr. move: (RSa gxr) => agxr. set v0 := BRabs (g x) +r \1r. have v0p: inc v0 BRps by apply:(RpsS_sum_r (RpSa gxr) RpsS1). set v1 := BRabs (g x) +r v0. have v1p: inc v1 BRps by exact :(RpsS_sum_r (RpSa gxr) v0p). set v2 := BRabs (f x) +r \1r. have v2a: BRabs (f x) <r v2 by exact:(BRsum_Mps (RSa fxr) RpsS1). have v2p: inc v2 BRps by apply:(RpsS_sum_r (RpSa fxr) RpsS1). move => e ep; move: (BRhalf_pos ep) => hep. set e1 := (BRhalf e) /r v1. set e2 := ((BRhalf e) /r v2). have e1ps: inc e1 BRps by apply:RpsS_div. have e2ps: inc e2 BRps by apply:RpsS_div. move:(rmin_prop2 e2ps v0p) (rmin_prop1 (BRps_sBR e2ps) (BRps_sBR v0p)). set e3:= (rmin e2 v0); move => e3ps [e3r e3a e3b]. move:(BRps_sBR hep) => her. have e3p1: e3 *r BRabs (f x) <r BRhalf e. move:(BRprod_Mltgt0 (RpsS_div hep v2p) v2a); rewrite BRprodC. rewrite (BRprod_div (BRps_sBR v2p) her (BRps_nz v2p)). move:(BRprod_Mlege0 (RpSa fxr) e3a) => sa sb; BRo_tac. move: (pa _ e1ps) => [d1 d1ps d1v]. move: (pb _ e3ps) => [d2 d2ps d2v]. move:(rmin_prop2 d1ps d2ps) (rmin_prop1 (BRps_sBR d1ps) (BRps_sBR d2ps)). set d3:= (rmin d1 d2); move => sa [sb sc sd]; ex_tac => y [yr ya]. have ha: BR_near x d1 y by split => //; BRo_tac. have hb: BR_near x d2 y by split => //; BRo_tac. move:(d1v _ ha)(d2v _ hb) => [fyr le1] [gyr le2]. have Ha: BRabs (f x *r (g x -r g y)) <r BRhalf e. rewrite (BRprod_abs fxr (RS_diff gxr gyr)). rewrite BRprodC; exact: (rle_ltT (BRprod_Mlege0 (RpSa fxr) le2) e3p1). move: (RS_diff gyr gxr) (RS_diff fxr fyr) => u1r u2r. have Hb: BRabs (g y) <=r v1. move:(rle_triangular u1r gxr). rewrite (BRsum_diff1 gxr gyr) (BRabs_diff gyr gxr). move/(BRsum_le2r (proj31 le2) (proj32 e3b) agxr): (rleT le2 e3b). rewrite (BRsumC v0) => hhb hhc; BRo_tac. have Hc: BRabs ((f x -r f y) *r g y) <=r BRhalf e. rewrite (BRprod_abs u2r gyr). move:(BRprod_Mlelege0 (BRps_sBRp e1ps) (RpSa gyr) le1 Hb). by rewrite (BRprodC _ v1) (BRprod_div(BRps_sBR v1p) her (BRps_nz v1p)). split; first by apply:RSp. move:(BRsum_Mlele (proj1 Ha) Hc); rewrite (BRdouble_half1 (BRps_sBR ep)). apply:rleT; move:(rle_triangular (RSp fxr (RS_diff gxr gyr)) (RSp u2r gyr)). move: (RSp fxr gxr) (RSp fxr gyr) (RSp fxr gyr) (RSp fyr gyr) => ar br cr dr. rewrite (BRprodBl gyr fxr fyr) (BRprodBr fxr gxr gyr). by rewrite (BRsumA (RS_diff ar br) br (RSo dr)) (BRsum_diff1 br ar). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)