proposition: Lemma Is_GreatestFixedPoint (f_monotonic : monotonic_function f) : fixed_point (cl_sup postfixed_point).
proof: Proof. pose proof Is_PostfixedPoint. apply f_monotonic in H. destruct (sup_lub postfixed_point). apply H0 in H. apply PO.le_antisym; eauto. apply Is_PostfixedPoint; eauto. eauto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat