proposition: Lemma BR_prodQ_aux x y: inc x BQps -> inc y BRps -> (BR_of_Q x) *r y = fun_image y (fun z => x *q z).
proof: Proof. move => xqps yps. have xips:=(RpsS_of_Q xqps). move/BRps_iP: (xips) => [_ xnz]. move/BRps_iP: (yps) => [_ ynz]. rewrite /BRprod; repeat Ytac0. move /BR_pos_prop: yps => [/BR_P [qa qb qc qd qe] [y' y'p y'y]]. have hb: forall t, inc t y -> y' <q t. move => t ty. case: (qleT_ell (qa _ ty) (BQps_sBQ y'p)) => lt1 //; case: y'y; try ue. apply: (qd _ _ ty lt1). have hb': forall t, inc t y -> inc t BQps. move => t /hb l1; apply/ qlt0xP; move / qlt0xP: y'p => l2;BQo_tac. move/BQps_iP: (xqps) => [ /BQp_sBQ xq xnz']. set_extens t. move => /BR_prod_auxP [z /Zo_P [zq xz] [u ub ->]]; apply /funI_P. have uq:= (hb' _ ub). move:(BQprod_Mltgt0 (QpsS_inv xqps) (BQprod_Mltgt0 uq xz)). rewrite -/(BQdiv _ _) (BQdiv_prod xq (BQps_sBQ uq) xnz') => h1. have h2:= (qd _ _ ub h1). by ex_tac; rewrite BQprod_div //; apply:QSp => //; apply: qa. move /funI_P => [z / qe [u uy l1] ->]; apply/BR_prod_auxP. have zq:=(proj32_1 l1). have up:=(hb' _ uy). move/BQps_iP: (up) => [ /BQp_sBQ uq unz]. move:(BQprod_Mltgt0 (QpsS_inv up) (BQprod_Mltgt0 xqps l1)). rewrite -/(BQdiv _ _) (BQdiv_prod uq xq unz) => h; move:(proj32_1 h) => h'. exists ((z *q x) *q BQinv u); first by apply:Zo_i. by ex_tac; rewrite BQprodC (BQprodC _ u) BQprod_div //; apply: QSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)