proposition: Lemma BQ_ltinv1 x: inc x BRps -> (x <r \1r <-> \1r <r BRinv x).
proof: Proof. move => h. move/BRps_iP: (h) => [/BRp_sBR xr xnz]. have h0: BRinv x *r x = \1r by rewrite BRprodC (BRprod_inv1 xr xnz). move:(BRps_sBRp (RpsS_inv h)) => h2. split => h1. case:(rleT_ell RS1 (BRp_sBR h2)) => // h3. by case: (proj2 h1);move:(BRinv_K xr); rewrite - h3 BRinv_1. by move:(proj2 (BRprod_Mltltgt0 RpsS1 h h3 h1)); rewrite h0 (BRprod_1r RS1). case:(rleT_el RS1 xr) => // h3. by move: (proj2 (BRprod_Mltpp h2 h3 h1)); rewrite h0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)