Proposition least_fixpoint_scott_continuous_map_is_least_fixpoint_on_N {X : dcppo} (f : scott_continuous_map X X) (n : ℕ) : pr1 (least_fixpoint_scott_continuous_map_on_N n) f = bot_iteration_directed_set f n. Proof. induction n as [ | n IHn ]. - apply idpath. - refine (_ @ maponpaths _ IHn). simpl ; unfold prodtofuntoprod ; simpl. apply (iterate_on_pt_scott_continuous_map_fun_pt n f). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Examples.Fixpoints. Require Import UniMath.OrderTheory.DCPOs.Examples.Exponentials. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.