Coqで鳩の巣原理の証明

(* (* Logic_J.v の独自(<=)を使う場合はこの中身が必要 *)
Lemma lt_irrefl : forall n, ~ n < n.
Proof.
 induction n.
 intro. inversion H.

 intro. destruct IHn.
 apply Sn_le_Sm__n_le_m. apply H.
Qed.

Lemma lt_not_le: forall n m : nat, n < m -> ~ m <= n.
Proof.
 intros.
 induction H.
 apply lt_irrefl.

 intro. destruct IHle. inversion H0.
 apply le_S. apply le_n.

 rewrite <- H2 in H0. apply le_S. apply Sn_le_Sm__n_le_m. apply H0.
Qed. 
*)Lemmaaux1:forall{X:Type}(x:X)xsl1l2,(foralla,appears_ina(x::xs)->appears_ina(l1++(x::l2)))->~repeats(x::xs)->foralla,appears_inaxs->appears_ina(l1++l2).Proof.intros.destruct(appears_in_appl1(x::l2)a(Ha(ai_lateraxxsH1))).applyapp_appears_in.left.applyH2.applyapp_appears_in.right.inversionH2.destructH0.rewrite<-H4.applyRP_hd.applyH1.applyH4.Qed.Lemmaaux2:forall{X:Type}xsys,(foralla:X,appears_inaxs->appears_inays)->~repeatsxs->lengthxs<=lengthys.Proof.introsXxs.inductionxs;intros.applyO_le_n.destruct(appears_in_app_split__(Hx(ai_here__)))as[l1].destructH1as[l2].rewriteH1.rewriteapp_length.simpl.rewrite<-plus_n_Sm.applyn_le_m__Sn_le_Sm.rewrite<-app_length.applyIHxs.(*ここで(l1++l2)についてIHを使う*)intros.rewriteH1inH.apply(aux1____HH0).applyH2.intro.destructH0.applyRP_tl.applyH2.Qed.Theorempigeonhole_principle:forall{X:Type}(l1l2:listX),excluded_middle->(forallx,appears_inxl1->appears_inxl2)->lengthl2<lengthl1->repeatsl1.Proof.intros.Check(H(repeatsl1)).destruct(H(repeatsl1));[assumption|].(* 背理法 *)destruct(lt_not_le__H1).applyaux2;[applyH0|applyH2].Qed.