proposition: Proposition iterate_on_pt_scott_continuous_map_fun_pt {X : dcpo} (n : ℕ) (f : scott_continuous_map X X) (x : X) : iterate_on_pt_scott_continuous_map n (f x ,, f) = f (iterate_on_pt_scott_continuous_map n (x ,, f)).
proof: Proof. revert x. induction n as [ | n IHn ]. - intro ; cbn. apply idpath. - intro x. simpl ; unfold prodtofuntoprod ; simpl. apply IHn. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Examples.Fixpoints UniMath.OrderTheory.DCPOs.Examples.Exponentials UniMath.OrderTheory.DCPOs.Examples.BinaryProducts