proposition: Lemma BRprodDr x y z: realp x -> realp y -> realp z -> x *r (y +r z) = (x *r y) +r (x *r z).
proof: Proof. move: x y z. pose W x y z := x *r (y +r z) = (x *r y) +r (x *r z). have HH: forall x, inc x BRps -> sub x BQps. move => x /BR_pos_prop [xR [w / qlt0xP wp nnx]] u ux. move: (BRi_sQ xR ux) => /BQ_i2P [] // / qge0xP nu. case:nnx;apply:(BRi_segment xR ux); BQo_tac. 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 zp) (BR_prod_aux1 xp yp). rewrite (BR_prod_aux1 xp (RpsS_sum_rl yp zp)). 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 [aa /BR_sump [b iby [c cz ->]]] ->]. rewrite (BQprodDr (ta _ ax) (tb _ iby) (tc _ cz)). apply/BR_sump;exists (a *q b); first by apply/BR_prod_auxP; ex_tac; ex_tac. exists (a *q c); [ by apply/BR_prod_auxP; ex_tac; ex_tac | done]. move => /BR_sump [ab /BR_prod_auxP [a ax [b iby eq1]]]. move => [ac /BR_prod_auxP [a' a'x [c cz eq2]] ->]. rewrite eq1 eq2. move: (HH _ xp _ ax) (HH _ xp _ a'x) => ap a'p. move/BQps_iP: (ap) => [ /BQp_sBQ aq anz]. move/BQps_iP: (a'p) => [ /BQp_sBQ a'q a'nz]. move: (tb _ iby) (tc _ cz) => bq cq. case: (qleT_el aq a'q) => le1. have ha: inc ((c *q a') /q a) z. case:(equal_or_not a a') => eq3; first rewrite eq3 BQprodC BQdiv_prod //. move:(BQprod_Mltgt0 (HH _ zp _ cz) (conj le1 eq3)) => lt2. move:(BQprod_Mltgt0 (QpsS_inv ap) lt2). rewrite -/(_ /q _) (BQdiv_prod aq cq anz) (BQprodC a') => lt3. by apply:(BRi_segment (BRps_sBR zp) cz). have ->: a' *q c = a *q ((c *q a') /q a). by rewrite BQprodC BQprod_div => //; apply:QSp. rewrite - (BQprodDr aq bq (tc _ ha)). apply/BR_prod_auxP; exists a => //; exists (b +q (c *q a') /q a) => //. apply /BR_sump; ex_tac;ex_tac. have ha: inc ((b *q a) /q a') y. move:(BQprod_Mltgt0 (HH _ yp _ iby) le1) => lt2. move:(BQprod_Mltgt0 (QpsS_inv a'p) lt2). rewrite -/(_ /q _) (BQdiv_prod a'q bq a'nz) (BQprodC a) => lt3. by apply:(BRi_segment (BRps_sBR yp) iby). have ->: a *q b = a' *q ((b *q a) /q a'). by rewrite BQprodC BQprod_div => //;apply:QSp. rewrite - (BQprodDr a'q (tb _ ha) cq). apply/BR_prod_auxP; exists a' => //; exists ((b *q a) /q a' +q c) => //. apply /BR_sump; ex_tac;ex_tac. have Hb: forall x y z, inc x BRps -> inc y BRms -> inc z BRms -> W x y z. move => x y z xp yn zn. move:(BRps_sBR xp)(BRms_sBR yn)(BRms_sBR zn) => xr yr zr. move: (Ha _ _ _ xp (BRopp_negative1 yn) (BRopp_negative1 zn)). move:(RSs yr zr) (RSp xr yr) (RSp xr zr) => sa sb sc. rewrite /W -(BRoppD yr zr) - ! BRopp_prod_r // -(BRoppD sb sc). by apply:BRopp_inj; [apply:RSp | apply:RSs]. suff Hw :(forall x y z, inc x BRps -> realp y -> inc z BR -> W x y z). move => x y z /BR_i1P [] xn yr zr. + by rewrite xn !BRprod_0l (BRsum_0l RS0). + by apply: Hw. + move: (BRms_sBR xn) => xr. move: (Hw _ _ _ (BRopp_negative1 xn) (RSo yr) (RSo zr)); rewrite /W. by rewrite - BRoppD //! BRprod_opp_opp //; apply:RSs. suff Hv :(forall x y z, inc x BRps -> inc y BRps -> inc z BRms -> W x y z). move => x y z xp /BR_i1P [] yr zr. + rewrite /W yr BRprod_0r (BRsum_0l zr) BRsum_0l //. by apply: RSp => //; apply:BRps_sBR. + case/BR_i1P: zr => w. - rewrite /W w BRprod_0r (BRsum_0r (BRps_sBR yr)) BRsum_0r//. by apply: RSp => //; apply:BRps_sBR. - by apply:Ha. - by apply:Hv. + case/BR_i1P: zr => w. - rewrite /W w BRprod_0r (BRsum_0r (BRms_sBR yr)) BRsum_0r //. by apply: RSp; [ apply:BRps_sBR | apply:BRms_sBR]. - rewrite /W BRsumC (BRsumC (x *r y)); by apply: Hv. - by apply: Hb. move => x y z xp yp zp. move:(BRps_sBR xp) (BRps_sBR yp) (BRms_sBR zp) => xr yr zr. have xyr:= RSp xr yr. have xzr:= RSp xr zr. have ha: realp (x *r (y +r z)) by apply: RSp => //; apply:RSs. have hb: realp (x *r (z +r y)) by apply: RSp => //; apply:RSs. case/BR_i1P: (RSs yr zr) => syz. + rewrite /W syz BRprod_0r. move: (BRdiff_xx_rw yr (RSo zr)); rewrite /BRdiff (BRopp_K zr) => h. rewrite (h syz) - (BRopp_prod_r xr zr) BRsumC BRsum_opp_r //. + move:(Ha _ _ _ xp syz (BRopp_negative1 zp)). rewrite /W -/(_ -r _) BRsumC (BRdiff_sum zr yr) => ->. by rewrite - (BRopp_prod_r xr zr) - /(_ -r _) (BRsumC _(x *r z)) BRsum_diff. + move:(Hb _ _ _ xp syz (BRopp_positive1 yp)). rewrite /W -/( _ -r _) (BRdiff_sum yr zr) => ->. rewrite - (BRopp_prod_r xr yr) - /(_ -r _) BRsum_diff //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)