apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
intros.apply le_n_O_to_eq.assumption.
intros.apply False_ind.apply (not_le_Sn_O ? H).
apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
intros.apply le_n_O_to_eq.assumption.
intros.apply False_ind.apply (not_le_Sn_O ? H).