proposition: Lemma lfp_eq : lfp == f lfp.
proof: Proof. unfold lfp. set (P x := f x <= x). set (a := glb P). destruct (glb_ok P) as [a_inf a_glb]. assert (Pa : f a <= a). apply a_glb. intros x Px. trans (f x). apply f_mon. apply a_inf. hyp. hyp. assert (h : a <= f a). apply a_inf. apply f_mon. hyp. fo. Qed.
imports: CoLoR(LogicUtil RelUtil SetUtil) Coq(Morphisms Basics)