no goals
x y : Nat
⊢ y > 0 → x % y < y
induction x, y using mod.inductionOn with
| base x y h₁ =>
  intro h₂
  have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.not_and_iff_or_not _ _) h₁
  match h₁ with
  | Or.inl h₁ => exact absurd h₂ h₁
  | Or.inr h₁ =>
    have hgt : y > x := gt_of_not_le h₁
    have heq : x % y = x := mod_eq_of_lt hgt
    rw [← heq] at hgt
    exact hgt
| ind x y h h₂ =>
  intro h₃
  have ⟨_, h₁⟩ := h
  rw [mod_eq_sub_mod h₁]
  exact h₂ h₃
case base
x y : Nat
h₁ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
⊢ x % y < y
case base
x y : Nat
h₁ : ¬(0 < y ∧ y ≤ x)
⊢ y > 0 → x % y < y
intro h₂
case base
x y : Nat
h₁✝ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁ : ¬0 < y ∨ ¬y ≤ x
⊢ x % y < y
case base
x y : Nat
h₁ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
⊢ x % y < y
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.not_and_iff_or_not _ _) h₁
no goals
case base
x y : Nat
h₁✝ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁ : ¬0 < y ∨ ¬y ≤ x
⊢ x % y < y
match h₁ with
| Or.inl h₁ => exact absurd h₂ h₁
| Or.inr h₁ =>
  have hgt : y > x := gt_of_not_le h₁
  have heq : x % y = x := mod_eq_of_lt hgt
  rw [← heq] at hgt
  exact hgt
no goals
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬0 < y
⊢ x % y < y
exact absurd h₂ h₁
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
⊢ x % y < y
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
⊢ x % y < y
have hgt : y > x := gt_of_not_le h₁
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
heq : x % y = x
⊢ x % y < y
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
⊢ x % y < y
have heq : x % y = x := mod_eq_of_lt hgt
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x % y
heq : x % y = x
⊢ x % y < y
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
heq : x % y = x
⊢ x % y < y
rw [← heq] at hgt
no goals
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x % y
heq : x % y = x
⊢ x % y < y
exact hgt
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
⊢ x % y < y
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
⊢ y > 0 → x % y < y
intro h₃
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ x % y < y
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
⊢ x % y < y
have ⟨_, h₁⟩ := h
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ (x - y) % y < y
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ x % y < y
rw [mod_eq_sub_mod h₁]
no goals
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ (x - y) % y < y
exact h₂ h₃