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