proposition: Lemma BR_gleP x y: gle BR_order x y <-> x <=r y.
proof: Proof. split; first by move/opp_gleP => /sub_gleP [pa pb pc]; split. by move => [pa pb pc]; apply/opp_gleP /sub_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)