proposition: Lemma iter'_isdirected (D : dcpowithbottom) : isdirected (@iter' D).
proof: 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.
imports: UniMath.Foundations.All