proposition: Lemma BRinv_mon2 a b: inc a BRps -> inc b BRps -> (BRinv a <r BRinv b <-> b <r a).
proof: Proof. move => pa pb; split; move => [ha hb]; split. + by apply /BRinv_mon1. + by dneg h; rewrite h. + by apply /BRinv_mon1. + by move /(BRinv_inj (BRps_sBR pa) (BRps_sBR pb)) => /nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)