proposition: Lemma Is_PrefixedPoint (f_monotonic : monotonic_function f) : prefixed_point (cl_inf prefixed_point).
proof: Proof. unfold prefixed_point at 1. destruct (inf_glb prefixed_point). apply H0. intros. unfold prefixed_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