Lemma iter'_increases (D : dcpowithbottom) : ∏ (n m : nat), (n ≤ m)%nat -> (@iter' D n ≤ @iter' D m). Proof. intros n m ineq. induction m as [ | m' IH]. - set (nis0 := natleh0tois0 ineq). rewrite nis0. apply isrefl_posetRelation. - set (cases := natlehchoice _ _ ineq). induction cases as [less | equal]. + eapply istrans_posetRelation. * apply IH. apply less. * apply iter'_isomegachain. + rewrite equal. apply isrefl_posetRelation. Qed.
Require Import UniMath.Foundations.All.