+(* le and eq *)
+lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
+apply nat_elim2
+ [intros.apply le_n_O_to_eq.assumption
+ |intros.apply sym_eq.apply le_n_O_to_eq.assumption
+ |intros.apply eq_f.apply H
+ [apply le_S_S_to_le.assumption
+ |apply le_S_S_to_le.assumption
+ ]
+ ]
+qed.
+