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