Lemma iter'_isomegachain (D : dcpowithbottom) : ∏ (n : nat), (@iter' D n ≤ @iter' D (S n)). Proof. induction n as [ | m IH]. - simpl. intro f. apply dcpowithbottom_isMinimal. - simpl. intro f. apply dcpomorphism_preservesorder. use IH. Qed.
Require Import UniMath.Foundations.All.