proposition: Lemma BR_tor: total_order BR_order.
proof: Proof. have [or sr]:=BR_osr. split => // x y; rewrite sr => xr yr. suff: sub x y \/ sub y x. by case => h; [right | left]; apply/opp_gleP; apply/sub_gleP. case(p_or_not_p (sub x y)) => h; first by left. have [a ax nay]: exists2 a, inc a x & ~inc a y. ex_middle bad; case h => b bx; ex_middle iby; case bad; ex_tac. right => b iby. case: (equal_or_not a b) => eab; first by case:nay; rewrite eab. case: (qleT_ee (BRi_sQ xr ax) (BRi_sQ yr iby)). by move => lab; move:(BRi_segment xr ax (conj lab eab)). move => lab; case: nay; exact: (BRi_segment yr iby (conj lab (nesym eab))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)