proposition: Lemma lift_complete : complete lift_order.
proof: Proof. intros c Hchain. exists (fun x => epsilon(inhabits (c 0 x))(fun v => lub R v (fun n => c n x))). apply lift_lub. intros x; apply epsilon_spec. apply Hc; apply chain_lift_reverse; assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith