proposition: Lemma RpsS_prod x y : inc x BRps -> inc y BRps -> inc (x *r y) BRps.
proof: Proof. move => sa sb; rewrite (BR_prod_aux1 sa sb); move: sa sb. move => /BR_pos_prop [xr [x' x'p x'x]] /BR_pos_prop [yr [y' y'p y'y]]. move: xr yr => /BR_P [pa pb pc pd pe] /BR_P [qa qb qc qd qe]. have ha: forall t, inc t x -> x' <q t. move => t tx. case: (qleT_ell (pa _ tx) (BQps_sBQ x'p)) => lt1 //; case: x'x; try ue. apply: (pd _ _ tx lt1). 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 hc: exists2 z, inc z BQps & ~ inc z (BRprod_aux x y). move: (QpsS_prod x'p y'p) => h; ex_tac => /BR_prod_auxP [u ua [v vb eq]]. move: (ha _ ua) (hb _ vb) => lt1 lt2. move:(proj2(BQprod_Mltltge0 (BQps_sBQp x'p) (BQps_sBQp y'p) lt1 lt2)); ue. have hb': forall t, inc t y -> inc t BQps. move => t /hb l1; apply/ qlt0xP; move / qlt0xP: y'p => l2;BQo_tac. apply/BR_pos_prop; split; [apply/BR_P; split | exact]. + by move => t/BR_prod_auxP [z za [u ua ->]]; apply:QSp;[ apply:pa |apply: qa]. + move:pb qb => [a ax] [b iby]; exists (a *q b); apply/BR_prod_auxP. ex_tac; ex_tac. + move => h. by move:hc => [z /BQps_sBQ za]; rewrite h; case. + move => a b /BR_prod_auxP [z za [u ua zv]] l1; apply/BR_prod_auxP. move:(qa _ ua) (pa _ za)(proj32_1 l1) => uq zq bq. move: (hb' _ ua) => sa; move: (QpsS_inv sa) => he. have unz: u <> \0q by move/BQps_iP: sa => []. have aux: inc (b /q u) x. apply: (pd _ _ za); rewrite -(BQdiv_prod uq zq unz). by apply:(BQprod_Mltgt0 he); rewrite BQprodC - zv. by ex_tac; ex_tac; rewrite BQprodC (BQprod_div uq bq unz). + move =>a /BR_prod_auxP [z /pe [b bx bv] [u ua zv]]. move: (qa _ ua) (pa _ bx)(proj32_1 bv) => uq bq zq. move:(hb' _ ua) => up. have aux: b *q u <q a by rewrite zv; apply:BQprod_Mltgt0. exists (b *q u) => //;apply/BR_prod_auxP; ex_tac; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)