proposition: Lemma BQinv_mon2 a b: inc a BQps -> inc b BQps -> (BQinv a <q BQinv b <-> b <q a).
proof: Proof. move => pa pb; split; move => [ha hb]; split. + by apply /BQinv_mon1. + by dneg h; rewrite h. + by apply /BQinv_mon1. + by move /(BQinv_inj (BQps_sBQ pa) (BQps_sBQ pb)) => /nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)