proposition: Lemma Is_PostfixedPoint (f_monotonic : monotonic_function f) : postfixed_point (cl_sup postfixed_point).
proof: Proof. unfold postfixed_point at 1. destruct (sup_lub postfixed_point). apply H0. intros. unfold postfixed_point in H1. eapply PreO.le_trans; eauto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat