proposition: Lemma Is_LeastFixedPoint (f_monotonic : monotonic_function f) : fixed_point (cl_inf prefixed_point).
proof: Proof. pose proof Is_PrefixedPoint. apply f_monotonic in H. destruct (inf_glb prefixed_point). apply H0 in H. apply PO.le_antisym; eauto. apply Is_PrefixedPoint; eauto. eauto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat