proposition: Lemma BQsum_Mlelt a b c d: a <=q c -> b <q d -> (a +q b) <q (c +q d).
proof: Proof. move => eq1 eq2; move: (proj32 eq1) (proj31_1 eq2)=> cz bz. move /(BQsum_le2r (proj31 eq1) cz bz): eq1 => eq3. move/(BQsum_lt2l bz (proj32_1 eq2) cz): eq2 => eq4. BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)