proposition: Lemma le_sup A B : A `<=` down B -> nonempty A -> has_sup B -> sup A <= sup B.
proof: Proof. move=> le_AB nz_A hs_B; have hs_A: has_sup A. split=> //; case: hs_B => _ [x ubx]. exists x; apply/ubP=> y /le_AB /downP[z zB le_yz]. by apply/(le_trans le_yz); move/ubP: ubx; apply. rewrite leNgt -subr_gt0; apply/negP => lt_sup. case: (sup_adherent lt_sup hs_A )=> x /le_AB xdB. rewrite subKr => lt_Bx; case/downP: xdB => z zB. move/(lt_le_trans lt_Bx); rewrite ltNge. by move/ubP : (sup_upper_bound hs_B) => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid