proposition: Lemma BQsum_AC x y z: ratp x -> ratp y -> ratp z -> (x +q y) +q z = (x +q z) +q y.
proof: Proof. move => xq yq zq. by rewrite - (BQsumA xq yq zq) - (BQsumA xq zq yq) (BQsumC y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)