suffixLevenshtein.proof_2
theorem suffixLevenshtein.proof_2 : 0 < Nat.succ 0
This theorem, `suffixLevenshtein.proof_2`, states that the number 1 (represented as `Nat.succ 0`, the successor of 0) is greater than 0. This is a fundamental and self-evident concept in the natural number system, where 1 is indeed greater than 0.
More concisely: The theorem `suffixLevenshtein.proof_2` asserts that `Nat.succ 0` is greater than `0` in Lean 4. In simpler terms, the statement is `1 > 0`.
|
suffixLevenshtein.proof_1
theorem suffixLevenshtein.proof_1 : ∀ {δ : Type u_1} (r : List δ), 0 < r.length.succ
The theorem `suffixLevenshtein.proof_1` states that for any list `r` of elements of an arbitrary type `δ`, the successor of the length of the list (`List.length r`) is greater than 0. In other words, adding 1 to the length of any list will always result in a number that is greater than zero. This is true in any case because the length of a list is non-negative (0 or a positive integer) and adding 1 to a non-negative number results in a positive number.
More concisely: For any list `r` of elements, the length of `r` plus one is a positive integer.
|