proposition: Lemma BQsum_cN n m: natp n -> natp m -> BQ_of_nat n +q BQ_of_nat m = BQ_of_nat (n +c m).
proof: Proof. move => sa sb; rewrite /BQ_of_nat - (BZsum_cN sa sb). by apply:BQsum_cZ;apply:BZ_of_nat_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)