fact: Definition Bourbaki_Witt_fixpoint_theorem_statement := LEM -> forall (P : Poset) (_ : is_chain_complete P) (f : Progressive_map P), Fixedpoint (pr1 f).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo