proposition: Lemma BQprod_sign x y: ratp x -> ratp y -> BQsign (x *q y) = (BQsign x) *z (BQsign y).
proof: Proof. move => xq yq. wlog h: x xq / inc x BQps. move => H; case/BQ_i1P:(xq) => xz. + by rewrite xz (BQprod_0l yq) ! BQsign_0 BZprod_0l. + by apply: H. + move:(H _ (QSo xq) (BQopp_negative1 xz)). have pa: intp (BQsign (x *q y)) by apply:ZS_sign. have pb: intp (BQsign x) by apply:ZS_sign. have pc: intp (BQsign y) by apply:ZS_sign. rewrite - (BQopp_prod_l xq yq) (BQopp_sign (QSp xq yq)) (BQopp_sign xq). by rewrite - BZopp_prod_l //; apply: BZopp_inj => //;apply: ZSp. move:ZS1 ZSm1=> z1 zz1;case/BQ_i1P:(yq) => yz. + by rewrite yz (BQprod_0r xq) ! BQsign_0 BZprod_0r. + by rewrite ! BQsign_pos //; [ rewrite BZprod_1l | apply:QpsS_prod]. + rewrite (BQsign_pos h) (BQsign_neg yz) BZprod_1l //. by rewrite (BQsign_neg) //; apply:QpmsS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)