proposition: Lemma QSp x y: ratp x -> ratp y -> ratp (x *q y).
proof: Proof. move => /BQ_P [_ nx dx pd] /BQ_P [_ ny dy qd]. exact: (BQ_of_pair_prop4 (ZSp nx ny) (ZpsS_prod dx dy)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)