Lemma iter_preservesorder {D : dcpowithbottom} (f g : D --> D) : (f ≤ g) -> ∏ (n : nat), (iter n f ≤ iter n g). Proof. intros ineq n; induction n as [ | m IH]. - apply isrefl_posetRelation. - simpl. eapply istrans_posetRelation. + apply dcpomorphism_preservesorder. exact IH. + use ineq. Qed.
Require Import UniMath.Foundations.All.