proposition: Lemma antisymmetric_lift : antisymmetric lift_order.
proof: Proof. intros f g HfRg HgRf. apply extensionality with (B:= fun x:A => B). intros x; apply (Ha (f x) (g x)); apply (HfRg x) || apply (HgRf x). Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith