proposition: Lemma BR_supremum_opp X a (x := supremum BR_order X): nonempty X -> (forall t, inc t X -> t <=r a) -> x = BRopp (infimum BR_order (fun_image X BRopp)).
proof: Proof. move => sa sb. move:BR_osr => [or sr]. have ha': sub X BR by move => t /sb []. have asr: inc a (substrate BR_order) by rewrite sr;move: (sa) => [u /sb []]. have ha: sub (fun_image X BRopp) BR. by move => t /funI_P [z /ha' za ->]; apply:RSo. have hb: nonempty (fun_image X BRopp) by apply: funI_setne. have hc': bounded_above BR_order X by exists a; split => // y /sb /BR_gleP. have hc: bounded_below BR_order (fun_image X BRopp). exists (BRopp a); split; first by move:asr; rewrite sr => /RSo. by move => y /funI_P [t /sb tx ->]; apply/BR_gleP/ rle_opp. have hd: sub (fun_image X BRopp) (substrate BR_order) by ue. have hd': sub X (substrate BR_order) by ue. move: (infimum_pr or hd (BR_inf_exists ha hb hc)). move: (supremum_pr or hd' (BR_sup_exists ha' sa hc')). rewrite -/x; set y := infimum _ _; move => [[ra1 ra2] rb][[rc1 rc2] rd]. have : upper_bound BR_order X (BRopp y). split; first by move: rc1;rewrite sr => /RSo. move => t tx. have: inc (BRopp t) (fun_image X BRopp) by apply/funI_P; ex_tac. by move / rc2 /BR_gleP/ rle_opp; rewrite (BRopp_K (ha' _ tx)) => /BR_gleP. move / rb /BR_gleP => le1. apply: rleA => //; rewrite - (BRopp_K (proj31 le1)); apply: rle_opp. have : lower_bound BR_order (fun_image X BRopp) (BRopp x). split;first by move: ra1;rewrite sr => /RSo. by move => t /funI_P [z / ra2/BR_gleP zX ->]; apply/BR_gleP/ rle_opp. by move / rd /BR_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)