Proposition is_fixpoint_least_fixpoint : f least_fixpoint = least_fixpoint. Proof. unfold least_fixpoint. rewrite scott_continuous_map_on_lub. use antisymm_dcpo. - use dcpo_lub_is_least. cbn ; intro i. use less_than_dcpo_lub. + exact (S i). + apply refl_dcpo. - use dcpo_lub_is_least. cbn ; intro i. use less_than_dcpo_lub. + exact i. + apply is_monotone_bot_iteration_map_S. 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.