proposition: Lemma infimum_BRp:infimum BR_order BRp = \0r.
proof: Proof. have [or sr] := BR_osr. have sr':sub BRp (substrate BR_order) by rewrite sr; apply:BRp_sBR. symmetry; apply:infimum_pr2 => //;apply/(glbP or) => //; split. by hnf; rewrite sr; split;[ apply:RS0 | move => y / rle0xP /BR_gleP]. move => z []; rewrite sr => zr; apply; apply: RpS0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)