The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

Hi,

here is another proof by inspection of all possible cases:

Goal forall n m:Z, Zmin n m = Zmin m n.
unfold Zmin; intros.
generalize(Zcompare_antisym m n).
generalize(Zcompare_Eq_eq m n).
destruct(n?=m); destruct(m?=n);
intuition; discriminate.
Qed.

Best,

Roland