proposition: Theorem lub_cst : forall (A:Type)(R:A->A->Prop)(a:A),(forall x, R x x)->lub R a (fun n=>a).
proof: Proof. intros A R a Hrefl. split. intros n; apply Hrefl. intros v Hup. apply (Hup 0). Qed.
imports: Relations Classical ClassicalEpsilon Zwf function_cpo