no goals
x y : Nat
⊢ x % y ≤ x
match Nat.lt_or_ge x y with
| Or.inl h₁ => rw [mod_eq_of_lt h₁]; apply Nat.le_refl
| Or.inr h₁ => match eq_zero_or_pos y with
  | Or.inl h₂ => rw [h₂, Nat.mod_zero x]; apply Nat.le_refl
  | Or.inr h₂ => exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁
x y : Nat
h₁ : x < y
⊢ x ≤ x
x y : Nat
h₁ : x < y
⊢ x % y ≤ x
rw [mod_eq_of_lt h₁]
no goals
x y : Nat
h₁ : x < y
⊢ x ≤ x
apply Nat.le_refl
no goals
x y : Nat
h₁ : x ≥ y
⊢ x % y ≤ x
match eq_zero_or_pos y with
| Or.inl h₂ => rw [h₂, Nat.mod_zero x]; apply Nat.le_refl
| Or.inr h₂ => exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁
x y : Nat
h₁ : x ≥ y
h₂ : y = 0
⊢ x ≤ x
x y : Nat
h₁ : x ≥ y
h₂ : y = 0
⊢ x % y ≤ x
rw [h₂, Nat.mod_zero x]
no goals
x y : Nat
h₁ : x ≥ y
h₂ : y = 0
⊢ x ≤ x
apply Nat.le_refl
no goals
x y : Nat
h₁ : x ≥ y
h₂ : y > 0
⊢ x % y ≤ x
exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁