Theorem is_least_fixpoint_least_fixpoint (x : X) (p : f x = x) : least_fixpoint ⊑ x. Proof. use dcpo_lub_is_least ; cbn. intro n. induction n as [ | n IHn ]. - apply is_min_bottom_dcppo. - rewrite <- p. exact (is_monotone_scott_continuous_map f IHn). 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.