Theorem: Int.div2_succ_le_self (ECTate/Algebra/EllipticCurve/Kronecker.lean)

State before:
x : ℕ
⊢ Nat.succ x / 2 ≤ x
Tactic:
cases x with
| zero => simp
| succ x =>
  exact (div_succ_le_succ_div (Nat.succ x) 1).trans (succ_le_of_lt (div2_lt_self (succ_pos x)))
State after:
no goals

State before:
case zero

⊢ Nat.succ zero / 2 ≤ zero
Tactic:
simp
State after:
no goals

State before:
case succ
x : ℕ
⊢ Nat.succ (Nat.succ x) / 2 ≤ Nat.succ x
Tactic:
exact (div_succ_le_succ_div (Nat.succ x) 1).trans (succ_le_of_lt (div2_lt_self (succ_pos x)))
State after:
no goals