proposition: Lemma lift_lub : forall (f:A->B)(c:nat->A->B), (forall x, lub R (f x)(fun n=> c n x))-> lub lift_order f c.
proof: Proof. intros f c Hx; split. intros n x; destruct (Hx x) as [Hu Hl]; apply Hu. intros g Hug x; destruct (Hx x) as [_ Hl]; apply Hl. intros n; apply (Hug n x). Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith