Definition leastfixedpoint {D : dcpowithbottom} : (D --> D) --> D. Proof. use make_dcpomorphism. - eapply pointwiselub. apply iter'_isdirected. - apply pointwiselub_isdcpomorphism'. Defined.
Require Import UniMath.Foundations.All.