proposition: Lemma BRprod_cQ x y: ratp x -> ratp y -> BR_of_Q x *r BR_of_Q y = BR_of_Q (x *q y).
proof: Proof. pose r x y := BR_of_Q x *r BR_of_Q y = BR_of_Q (x *q y). have H: forall x y, inc x BQps -> inc y BQps -> r x y. move => u v up vp. rewrite /r (BR_prodQ_aux up (RpsS_of_Q vp)); set_extens t. move /funI_P => [z /Zo_P [za zb] ->]; apply/Zo_P; split. by apply:QSp => //; apply: BQps_sBQ. by rewrite BQprodC (BQprodC u); apply:BQprod_Mltgt0. move/BQps_iP: (up) => [ /BQp_sBQ uq unz]. move/BQps_iP: (vp) => [ /BQp_sBQ vq vnz]. move => /Zo_P [tq lt]; apply/funI_P. move: (BQprod_Mltgt0 (QpsS_inv up) lt). rewrite -/( _/q _) (BQdiv_prod uq vq unz) => sa; exists (t /q u). apply:Zo_i => //; rewrite -/(ratp _);BQo_tac. by rewrite (BQprod_div uq tq unz). have H2: forall x y, inc x BQps -> ratp y -> r x y. move => u v up vq;move: (BQps_sBQ up) => uq; case/(BQ_i1P): (vq) => ha. + by rewrite /r ha (BQprod_0r uq) -/ BR_zero BRprod_0r. + by apply: H. + move:(RS_of_Q uq)(RS_of_Q vq) (RS_of_Q (QSp uq vq)) => sa sb sc. move:(H u (BQopp v) up (BQopp_negative1 ha)). rewrite /r - (BQopp_prod_r uq vq) - (BRopp_Q vq). rewrite - (BRopp_Q (QSp uq vq)) - (BRopp_prod_r sa sb). by move /(BRopp_inj (RSp sa sb) sc). case/BQ_i1P => h yq. + by rewrite h (BQprod_0l yq) -/ BR_zero BRprod_0l. + by apply: H2. + move:(BQms_sBQ h) => ha;move:(H2 _ _ (BQopp_negative1 h) (QSo yq)). rewrite /r (BQprod_opp_opp ha yq) - !(BRopp_Q) //. by rewrite (BRprod_opp_opp (RS_of_Q ha) (RS_of_Q yq)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)