proposition: Lemma BRinv_mon1 a b: inc a BRps -> inc b BRps -> (BRinv a <=r BRinv b <-> b <=r a).
proof: Proof. move => pa pb. rewrite - (BRdiv_1x (BRps_sBR pa)) - (BRdiv_1x (BRps_sBR pb)). apply: (BRinv_mon pa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)