pith. machine review for the scientific record. sign in
lemma proved tactic proof

int_natAbs_eq_one_of_nonneg

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 757private lemma int_natAbs_eq_one_of_nonneg {z : ℤ} (hz : Int.natAbs z = 1) (hznn : 0 ≤ z) :
 758    z = 1 := by

proof body

Tactic-mode proof.

 759  cases z with
 760  | ofNat n =>
 761      -- natAbs (ofNat n) = n
 762      have : n = 1 := by simpa using hz
 763      simpa [this]
 764  | negSucc n =>
 765      -- negative contradiction
 766      have : ¬ (0 ≤ Int.negSucc n) := by
 767        -- `negSucc n = -(n+1) < 0`
 768        have : Int.negSucc n < 0 := by
 769          simpa using (Int.negSucc_lt_zero n)
 770        exact not_le_of_gt this
 771      exact (this hznn).elim
 772

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.