Proposition least_fixpoint_scott_continuous_map_is_least_fixpoint {X : dcppo} (f : scott_continuous_map X X) : pr1 (least_fixpoint_scott_continuous_map X) f = least_fixpoint f. Proof. use antisymm_dcpo. - use dcpo_lub_is_least. intro i ; cbn in i. use less_than_dcpo_lub. + exact i. + rewrite <- least_fixpoint_scott_continuous_map_is_least_fixpoint_on_N. apply refl_dcpo. - use dcpo_lub_is_least. intro i ; cbn in i. use less_than_dcpo_lub. + exact i. + rewrite <- least_fixpoint_scott_continuous_map_is_least_fixpoint_on_N. apply refl_dcpo. 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.