proposition: Lemma has_sup_down A : has_sup (down A) <-> has_sup A.
proof: Proof. split=> -[nzA nzubA]. case: nzA => x /downP[y yS le_xy]; split; first by exists y. case: nzubA=> u /ubP ubA; exists u; apply/ubP=> z zS. by apply/ubA; apply/downP; exists z. case: nzA => x xA; split; first by exists x; apply/le_down. case: nzubA => u /ubP ubA; exists u; apply/ubP=> y /downP []. by move=> z zA /le_trans; apply; apply/ubA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid