proposition: Lemma least_unique : antisymmetric R -> forall (P : A -> Prop)(x y: A), P x /\ (forall z, P z -> R x z) -> P y /\ (forall z, P z -> R y z) -> x = y.
proof: Proof. intuition. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith