proposition: Lemma continuous2_prod : continuous2 BRprod.
proof: Proof. apply:continuous2_sym; first by move => x y _ _ ;apply: BRprodC. move => x y xr yr e ep. set e1 := Yo (x = \0r) \1r (e /r (BRabs x)). have ha : x <> \0r -> BRabs x <> \0r by move/(BRabs0_bis xr). have e1p: inc e1 BRps. rewrite /e1; Ytac h; [ apply: RpsS1 |apply:(RpsS_div ep); apply/BRps_iP ]. split; [apply: (RpSa xr) | by apply: ha]. ex_tac; move=> z [zr zb]; split; first by apply:RSp. rewrite - (BRprodBr xr yr zr) (BRprod_abs xr (RS_diff yr zr)). case: (equal_or_not x \0r) => sa. rewrite sa BRabs_0 BRprod_0l; apply/ rle0xP => //; exact:(BRps_sBRp ep). move: (BRprod_Mlege0 (RpSa xr) zb); rewrite BRprodC /e1; Ytac0. by rewrite (BRprodC _ (BRabs x)) (BRprod_div (RSa xr) (BRps_sBR ep) (ha sa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)