proposition: Lemma BQps_stable_prod1 a b: ratp a -> ratp b -> inc (a *q b) BQps -> ((inc a BQps <-> inc b BQps) /\ (inc a BQms <-> inc b BQms)).
proof: Proof. move => aq bq. move:BQ_di_neg_spos => H. case /BQ_i1P: (aq) => pa; first by rewrite pa (BQprod_0l bq) => /BQps_iP [_]. case /BQ_i1P: bq; first by move ->; rewrite (BQprod_0r aq) => /BQps_iP [_]. move => pb pc;split; split => // h; [case: (H _ h pa) | case:(H _ h pb)]. move => pb pc;case: (H _ _ pc); exact: (QpmsS_prod pa pb). case /BQ_i1P: bq; first by move ->; rewrite (BQprod_0r aq) => /BQps_iP [_]. move => pb pc; case: (H _ _ pc); rewrite BQprodC; exact (QpmsS_prod pb pa). move => pb pc; split => //; split => h; [case: (H _ pa h) | case: (H _ pb h)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)