proposition: Lemma BRopp_prod_r x y: realp x -> realp y -> BRopp (x *r y) = x *r (BRopp y).
proof: Proof. move => xr yr. have or :=(BRopp_K yr). rewrite /BRprod. have H: y <> \0r -> ~ inc y BRps -> inc (BRopp y) BRps. by move => ha hb; case/(BR_i1P): yr => // /BRopp_negative1. case: (equal_or_not x \0r) => ha; first by rewrite !(Y_true ha) BRopp_0. rewrite !(Y_false ha). case: (equal_or_not y \0r) => hb. by rewrite !(Y_true hb) hb BRopp_0; Ytac0; Ytac0; rewrite !Y_same BRopp_0. have hc: (BRopp y <> \0r). by move => h; move:(f_equal BRopp h); rewrite or BRopp_0. rewrite !(Y_false hb) !(Y_false hc). case: (inc_or_not x BRps) => hd;[ rewrite !(Y_true hd) | rewrite !(Y_false hd)]. Ytac he; first by rewrite(Y_false (BR_di_neg_spos (BRopp_positive1 he))) or. move:(H hb he) => hf; Ytac0; rewrite - (BR_prod_aux1 hd hf). exact:(BRopp_K (BRps_sBR (RpsS_prod hd hf))). have oxp: inc (BRopp x) BRps by case/(BR_i1P): xr => // /BRopp_negative1. Ytac he; last by move:(H hb he) => hf; Ytac0. rewrite(Y_false (BR_di_neg_spos (BRopp_positive1 he))) or. rewrite - (BR_prod_aux1 oxp he). exact:(BRopp_K (BRps_sBR (RpsS_prod oxp he))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)