x : Nat
h : x % 1 < 1
⊢ x % 1 = 0
x : Nat
⊢ x % 1 = 0
have h : x % 1 < 1 := mod_lt x (by decide)
x : Nat
h : x % 1 < 1
this : ∀ (y : Nat), y < 1 → y = 0
⊢ x % 1 = 0
x : Nat
h : x % 1 < 1
⊢ x % 1 = 0
have : (y : Nat) → y < 1 → y = 0 := by
  intro y
  cases y with
  | zero   => intro _; rfl
  | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)
no goals
x : Nat
h : x % 1 < 1
this : ∀ (y : Nat), y < 1 → y = 0
⊢ x % 1 = 0
exact this _ h
no goals
x : Nat
⊢ 1 > 0
decide
x : Nat
h : x % 1 < 1
y : Nat
⊢ y < 1 → y = 0
x : Nat
h : x % 1 < 1
⊢ ∀ (y : Nat), y < 1 → y = 0
intro y
no goals
x : Nat
h : x % 1 < 1
y : Nat
⊢ y < 1 → y = 0
cases y with
| zero   => intro _; rfl
| succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)
case zero
x : Nat
h : x % 1 < 1
a✝ : zero < 1
⊢ zero = 0
case zero
x : Nat
h : x % 1 < 1
⊢ zero < 1 → zero = 0
intro _
no goals
case zero
x : Nat
h : x % 1 < 1
a✝ : zero < 1
⊢ zero = 0
rfl
case succ
x : Nat
h✝ : x % 1 < 1
y : Nat
h : succ y < 1
⊢ succ y = 0
case succ
x : Nat
h : x % 1 < 1
y : Nat
⊢ succ y < 1 → succ y = 0
intro h
no goals
case succ
x : Nat
h✝ : x % 1 < 1
y : Nat
h : succ y < 1
⊢ succ y = 0
apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)