Theorem: div_succ_le_succ_div (ECTate/Algebra/EllipticCurve/Kronecker.lean)

State before:
m n : ℕ
⊢ succ m / succ n ≤ succ (m / succ n)
Tactic:
rw [succ_div]
State after:
m n : ℕ
⊢ (m / succ n + if succ n ∣ m + 1 then 1 else 0) ≤ succ (m / succ n)

State before:
m n : ℕ
⊢ (m / succ n + if succ n ∣ m + 1 then 1 else 0) ≤ succ (m / succ n)
Tactic:
split
State after:
case inl
m n : ℕ
h✝ : succ n ∣ m + 1
⊢ m / succ n + 1 ≤ succ (m / succ n)

case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)

State before:
case inl
m n : ℕ
h✝ : succ n ∣ m + 1
⊢ m / succ n + 1 ≤ succ (m / succ n)

case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Tactic:
. rw [succ_eq_add_one]
State after:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)

State before:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Tactic:
. rw [add_zero]
  exact le_succ (m / succ n)
State after:
no goals

State before:
case inl
m n : ℕ
h✝ : succ n ∣ m + 1
⊢ m / succ n + 1 ≤ succ (m / succ n)
Tactic:
rw [succ_eq_add_one]
State after:
no goals

State before:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Tactic:
rw [add_zero]
State after:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n ≤ succ (m / succ n)

State before:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n ≤ succ (m / succ n)
Tactic:
exact le_succ (m / succ n)
State after:
no goals