proposition: Theorem antisymmetric_f_order : forall A B, antisymmetric (f_order A B).
proof: Proof. intros; unfold f_order; apply antisymmetric_lift; apply antisym_option_cpo. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith