proposition: Lemma BQsum_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:(QSs cz dz) (QSs bz dz)=> cdz bdz. by rewrite -!BQsumA // (BQsum_CA bz cz dz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)