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