proposition: Lemma BQprod_nz x y: ratp x -> ratp y -> x <> \0q -> y <> \0q -> x *q y <> \0q.
proof: Proof. move => xq yq xnz ynz. move: (xq)(yq) => /BQ_P [_ xn xd _] /BQ_P [_ yn yd _]. move / (BQ_of_pair_zero (ZSp xn yn) (ZpsS_prod xd yd)). apply:(BZprod_nz xn yn); [ by move/(BQnum0_P xq) | by move/(BQnum0_P yq)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)