proposition: Lemma BR_prodQ_aux1 x y: x <> \0r -> rationalp x -> irrationalp y -> irrationalp (x *r y).
proof: Proof. move => xnz xra. wlog: y/ inc y BRps. move => H yr; move /BR_P:(proj1 yr) => /BR_i1P; case => ha. + by move:(BR_of_Q_prop1 QS0); rewrite -/ BR_zero - ha; move => [_]. + by apply: H. + move:(RSIo (H _ (BRopp_negative1 ha) (RSIo yr))). move: (proj1 xra) => /BR_P xr; move: (BRms_sBR ha)=> yr'. by rewrite (BRopp_prod_r xr (RSo yr')) BRopp_K. move: xnz;move/BR_of_Q_prop2:xra => [a aq ->] anz1 ya yb. case: (equal_or_not a \0q) => anz; first by case: anz1; rewrite anz. clear anz1. have yr:=(BRps_sBR ya). wlog: a aq anz / inc a BQps. move => H; case /BQ_i1P:aq => // ha; first by apply:H => //; apply:BQps_sBQ. have hb:= BQopp_negative1 ha. have aq:= BQms_sBQ ha. have ar:= RS_of_Q aq. have hc: BQopp a <> \0q by rewrite -BQopp_0 => /(BQopp_inj aq QS0). move:(H _ (BQps_sBQ hb) hc hb). rewrite - (BRopp_Q aq) - (BRopp_prod_l ar yr) => /RSIo. by rewrite(BRopp_K (RSp ar yr)). move => ap; split; first by apply/BR_P;apply:(RSp (RS_of_Q aq) yr). rewrite (BR_prodQ_aux ap ya) => t /setC_P [tq] /funI_P h. case: (inc_or_not (t /q a) y) => tay. by case:h; ex_tac; rewrite BQprod_div. move:((proj2 yb) _ (setC_i (QS_div tq aq) tay)) => [b /setC_P [bq bb] bc]. move:(BQprod_Mltgt0 ap bc);rewrite BQprodC (BQprod_div aq tq anz) BQprodC => lt. exists (a *q b) => //; apply /setC_P; split;first by rewrite -/(ratp _);BQo_tac. move => /funI_P [z zy]. by move/(BQprod_eq2l aq bq (BRi_sQ yr zy)) => bz; case:bb; rewrite bz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)