proposition: Theorem complete_f_order : forall A B, complete (f_order A B).
proof: Proof. intros; unfold f_order; apply lift_complete; apply complete_option_cpo. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith