proposition: Lemma BQprod_ACA a b c d: ratp a -> ratp b -> ratp c -> ratp d -> (a *q b) *q (c *q d) = (a *q c) *q (b *q d).
proof: Proof. move => az bz cz dz; move: (QSp cz dz) (QSp bz dz)=> cdz bdz. by rewrite -!BQprodA // (BQprod_CA bz cz dz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)