shape — Mathlib

English

If n+1 ≠ m, then d(n,m) = 0.

Русский

Если n+1 не равно m, то d(n,m) = 0.

LaTeX

$$shape (n m : \mathbb{Z}) (hnm : n + 1 ≠ m) : h.d n m = 0$$

Lean4

theorem shape (n m : ℤ) (hnm : n + 1 ≠ m) : h.d n m = 0 :=
  match n, m with
  | .ofNat n, .ofNat m => L.shape _ _ (by simp at hnm ⊢; cutsat)
  | .negSucc n, .negSucc m => by simpa only [d_negSucc] using K.shape n m (by simp at hnm ⊢; cutsat)
  | .negSucc 0, .ofNat 0 => by simp at hnm
  | .ofNat _, .negSucc m => rfl
  | .negSucc n, .ofNat m => by
    obtain _ | n := n
    · obtain _ | m := m
      · simp at hnm
      · rfl
    · rfl

Похожие утверждения