proposition: Proposition pataraia_fixpoint_compose_lemma (g : progressive_map (post_fixpoint_dcpo f)) (x : post_fixpoint_dcpo f) : g(m x) = m x.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO