proposition: Lemma BQsum_Mlege0 a c d: a <=q c -> \0q <=q d -> a <=q (c +q d).
proof: Proof. by move => pa pb; move: (BQsum_Mlele pa pb);rewrite (BQsum_0r (proj31 pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)