wikipediaの証明のページにあるように
数学的帰納法や背理法などと同じ分類のものみたいですね
(演繹法が載ってないのは何故)

背理法は直観主義論理では排中律の仮定が必要であるように
数学的帰納法や鳩の巣箱の原理も
それを公理(推論規則？)として認めるか認めないかで
なんちゃら論理という分類があるのかと思い
上記のような質問をしました

調べたところcoqではこのように書けるそうですが
該当pdfには証明(or証明ができるのか)は載っていませんでした
Lemma pigeon_hole :
forall m n, m < n ->
forall f, (forall i, i < n -> f i < m) ->
exists i, i < n /\
exists j, j < n /\ i <> j /\ f i = f j.

これがcoqで証明出来るのであれば
直観主義論理においては鳩の巣箱の原理は定理といえそうですが
多分、そうじゃないですよね？
どなたかよろしくお願いします