fact: Definition isfixedpoint {P : Poset} (f : P -> P) : hsubtype P := fun (x:P) => f x = x.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo