proposition: Lemma gfp_eq : gfp == f gfp.
proof: Proof. unfold gfp. set (P x := x <= f x). set (a := lub P). destruct (lub_ok P) as [a_sup a_lub]. assert (Pa : a <= f a). apply a_lub. intros x Px. trans (f x). hyp. apply f_mon. apply a_sup. hyp. assert (h : f a <= a). apply a_sup. apply f_mon. hyp. fo. Qed.
imports: CoLoR(LogicUtil RelUtil SetUtil) Coq(Morphisms Basics)