proposition: Lemma BRprodA x y z: realp x -> realp y -> realp z -> x *r (y *r z) = (x *r y) *r z.
proof: Proof. move: x y z. pose W x y z := x *r (y *r z) = (x *r y) *r z. have Ha: forall x y z, inc x BRps -> inc y BRps -> inc z BRps -> W x y z. move => x y z xp yp zp. rewrite /W (BR_prod_aux1 xp (RpsS_prod yp zp))(BR_prod_aux1 yp zp). rewrite (BR_prod_aux1 (RpsS_prod xp yp) zp) (BR_prod_aux1 xp yp). move:(BRi_sQ (BRps_sBR xp))(BRi_sQ (BRps_sBR yp))(BRi_sQ (BRps_sBR zp)) => ta tb tc. set_extens t. move/BR_prod_auxP => [a ax [b /BR_prod_auxP [c cy [d dz -> ->]]]]. rewrite (BQprodA (ta _ ax) (tb _ cy) (tc _ dz)). apply/BR_prod_auxP; exists (a *q c); last by ex_tac. by apply/BR_prod_auxP; ex_tac; ex_tac. move/BR_prod_auxP => [u /BR_prod_auxP [a ax [b iby ->]] [c cz ->]]. rewrite - (BQprodA (ta _ ax) (tb _ iby) (tc _ cz)). apply/BR_prod_auxP; ex_tac;exists (b *q c) => //. apply/BR_prod_auxP; ex_tac; ex_tac. have Hb: forall x y z, inc x BRps -> inc y BRps -> realp z -> W x y z. move => x y z xp yp /BR_i1P [] zp. + by rewrite /W zp !BRprod_0r. + by apply: Ha. + move:(Ha _ _ _ xp yp (BRopp_negative1 zp)); rewrite /W. move: (BRps_sBR xp)(BRps_sBR yp)(BRms_sBR zp) => xr yr zr. move:(RSp yr zr) (RSp xr yr) => ha hb. by rewrite - !BRopp_prod_r // => /(BRopp_inj (RSp xr ha) (RSp hb zr)). have Hc: forall x y z, inc x BRps -> realp y -> realp z -> W x y z. move => x y z xp /BR_i1P [] yp zr. + by rewrite /W yp !(BRprod_0l,BRprod_0r). + by apply: Hb. + move:(Hb _ _ _ xp (BRopp_negative1 yp) zr); rewrite /W. move: (BRps_sBR xp)(BRms_sBR yp) => xr yr. move:(RSp yr zr) (RSp xr yr) => ha hb. rewrite - BRopp_prod_l // - !BRopp_prod_r // - BRopp_prod_l //. by move => /(BRopp_inj (RSp xr ha) (RSp hb zr)). move => x y z /BR_i1P [] xp yr zr. + by rewrite /W xp ! BRprod_0l. + by apply: Hc. + move:(Hc _ _ _ (BRopp_negative1 xp) yr zr); rewrite /W. move: (BRms_sBR xp) => xr. move:(RSp yr zr) (RSp xr yr) => ha hb. by rewrite - !BRopp_prod_l // => /(BRopp_inj (RSp xr ha) (RSp hb zr)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)