Lemma iter'_isdirected (D : dcpowithbottom) : isdirected (@iter' D). Proof. split. - apply hinhpr. exact O. - intros n m. apply hinhpr. exists (n + m). split. + apply iter'_increases. apply natlehnplusnm. + apply iter'_increases, natlehmplusnm. Qed.
Require Import UniMath.Foundations.All.