Proposition pataraia_fixpoint_compose_lemma (g : progressive_map (post_fixpoint_dcpo f)) (x : post_fixpoint_dcpo f) : g(m x) = m x. Proof. use antisymm_dcpo. - pose (le_largest_progressive_map (comp_progressive_map m g) x) as p. refine (trans_dcpo _ p). cbn -[largest_progressive_map]. apply refl_dcpo. - exact (progressive_map_is_progressive g (m x)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.