proposition: Lemma BQinv_mon1 a b: inc a BQps -> inc b BQps -> (BQinv a <=q BQinv b <-> b <=q a).
proof: Proof. move => pa pb. rewrite - (BQdiv_1x (BQps_sBQ pa)) - (BQdiv_1x (BQps_sBQ pb)). apply: (BQinv_mon pa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)