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

State before:
n : ℕ
⊢ succ (succ n) / 2 = succ (n / 2)
Tactic:
rw [succ_eq_add_one, succ_eq_add_one, add_assoc, add_div_eq_of_add_mod_lt, Nat.div_self (zero_lt_succ 1)]
State after:
n : ℕ
⊢ n % 2 + (1 + 1) % 2 < 2

State before:
n : ℕ
⊢ n % 2 + (1 + 1) % 2 < 2
Tactic:
rw [mod_self, add_zero]
State after:
n : ℕ
⊢ n % 2 < 2

State before:
n : ℕ
⊢ n % 2 < 2
Tactic:
exact mod_lt n (zero_lt_succ 1)
State after:
no goals