proposition: Lemma lfp_eq_lub : eq (lub K) lfp.
proof: Proof. eapply glb_is_uniq. 2: apply glb_ok. destruct (lub_ok K) as [h1 h2]. split. intros x hx. apply h2. induction 1. trans (f x). apply f_mon. hyp. hyp. destruct (lub_ok S) as [g1 g2]. apply g2. hyp. intros y hy. apply hy. apply h1. apply Kf. apply Klub. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SetUtil) Coq(Morphisms Basics)