proposition: Proposition is_fixpoint_pataraia_fixpoint : f pataraia_fixpoint = pataraia_fixpoint.
proof: Proof. unfold pataraia_fixpoint. pose (p := maponpaths pr1 (pataraia_fixpoint_compose_lemma (restriction_to_post_fixpoint f) (bot_post_fixpoint f))). refine (p @ _). apply idpath. 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