definition pred ≝
λn. match n with [ O ⇒ O | S p ⇒ p].
-theorem pred_Sn : ∀n. n = pred (S n).
+theorem pred_Sn : ∀n.n = pred (S n).
// qed.
theorem injective_S : injective nat nat S.
// qed.
*)
-theorem plus_n_O: ∀n:nat. n = n+O.
+theorem plus_n_O: ∀n:nat. n = n+0.
#n (elim n) normalize // qed.
theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.