-\begin{example}
-\begin{Verbatim}
-theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
- intros.
- cut (m+p \le n \or m+p \nleq n).
- elim Hcut.
- symmetry.
- apply plus_to_minus.
- rewrite > assoc_plus.
- rewrite > (sym_plus p).
- rewrite < plus_minus_m_m.
- rewrite > sym_plus.
- rewrite < plus_minus_m_m.
- reflexivity.
- apply (trans_le ? (m+p)).
- rewrite < sym_plus.
- apply le_plus_n.
- assumption.
- apply le_plus_to_minus_r.
- rewrite > sym_plus.
- assumption.
- rewrite > (eq_minus_n_m_O n (m+p)).
- rewrite > (eq_minus_n_m_O (n-m) p).
- reflexivity.
- apply le_plus_to_minus.
- apply lt_to_le.
- rewrite < sym_plus.
- apply not_le_to_lt.
- assumption.
- apply lt_to_le.
- apply not_le_to_lt.
- assumption.
- apply (decidable_le (m+p) n).
-qed.
-\end{Verbatim}
-\end{example}
+%\begin{example}
+%\begin{Verbatim}
+%theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
+% intros.
+% cut (m+p \le n \or m+p \nleq n).
+% elim Hcut.
+% symmetry.
+% apply plus_to_minus.
+% rewrite > assoc_plus.
+% rewrite > (sym_plus p).
+% rewrite < plus_minus_m_m.
+% rewrite > sym_plus.
+% rewrite < plus_minus_m_m.
+% reflexivity.
+% apply (trans_le ? (m+p)).
+% rewrite < sym_plus.
+% apply le_plus_n.
+% assumption.
+% apply le_plus_to_minus_r.
+% rewrite > sym_plus.
+% assumption.
+% rewrite > (eq_minus_n_m_O n (m+p)).
+% rewrite > (eq_minus_n_m_O (n-m) p).
+% reflexivity.
+% apply le_plus_to_minus.
+% apply lt_to_le.
+% rewrite < sym_plus.
+% apply not_le_to_lt.
+% assumption.
+% apply lt_to_le.
+% apply not_le_to_lt.
+% assumption.
+% apply (decidable_le (m+p) n).
+%qed.
+%\end{Verbatim}
+%\end{example}