proposition: Lemma BRprod_abs x y: realp x -> realp y -> BRabs (x *r y) = (BRabs x) *r (BRabs y).
proof: Proof. move => xr yr. case /BR_i0P: (xr)=> pa; case /BR_i0P: (yr)=> pb. + rewrite (BRabs_negs pa) (BRabs_negs pb) (BRprod_opp_opp xr yr). by rewrite (BRabs_poss (RmsuS_prod pa pb)). + rewrite (BRabs_negs pa) (BRabs_pos pb) - (BRopp_prod_l xr yr). by rewrite BRprodC (BRabs_neg (RpmS_prod pb (BRms_sBRm pa))). + rewrite (BRabs_negs pb) (BRabs_pos pa) - (BRopp_prod_r xr yr). by rewrite (BRabs_neg (RpmS_prod pa (BRms_sBRm pb))). + by rewrite (BRabs_pos pa) (BRabs_pos pb) (BRabs_pos (RpS_prod pa pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)