proposition: Lemma sup_down A : sup (down A) = sup A.
proof: Proof. have [supA|supNA] := pselect (has_sup A); last first. by rewrite !sup_out // => /has_sup_down. have supDA : has_sup (down A) by apply/has_sup_down. apply/eqP; rewrite eq_le !le_sup //. - by case: supA => -[x xA] _; exists x; apply/le_down. - by rewrite downK; exact: le_down. - by case: supA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid