proposition: Lemma BR_no_least x : ~ (least BR_order x).
proof: Proof. move => [xsr xl]. rewrite (proj2 BR_osr) in xsr xl. move/BR_P: (xsr) => [pa _ pc pd _]. have [a /setC_P [aq nax]] := (setC_ne (conj pa pc)). have h1:=(BQsum_Mms aq QmsSm1). move/(rlt_cQ (proj31_1 h1) (proj32_1 h1)): h1 => h2. have h3:=(rlt_leT h2 (BR_le_aux3 xsr aq nax)). move: (xl _ (proj31_1 h3)) => /BR_gleP h4; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)