n1,…,n100∈N
P1:　n2<n1 & n3<n1 … n99<n1 & n100<n1
P2:　n1<n2 & n3<n2 … n99<n2 & n100<n2
…
P99:　n1<n99 & n3<n99 … & n98<n99 & n100<n99
P100:　n1<n100 & n3<n100 … & n98<n100 & n99<n100
とする

このとき
任意のPi,Pj　(1<=i<j<=100)について¬(Pi＆Pj)　が成り立つ

上記をCoqもしくはMizarで証明せよ

(ヒント　基本的には¬(a<b & b<a)の証明)