|
Fail Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
match H1 with
| le_n => le_n (pred _)
| le_S _ H2 =>
match n2 with
| 0 => fun H3 => H3
| S _ => le_S _ _
end (le_pred _ _ H2)
end.
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
