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

State before:
x : ℕ
⊢ x ≠ 0 → 0 < (val_bin_nat x).snd
Tactic:
cases x with
| zero =>
  intro absurd
  apply False.elim
  apply absurd
  rfl
| succ x =>
  intro _
  exact odd_part_succ_pos x
State after:
no goals

State before:
case zero

⊢ zero ≠ 0 → 0 < (val_bin_nat zero).snd
Tactic:
intro absurd
State after:
case zero
absurd : zero ≠ 0
⊢ 0 < (val_bin_nat zero).snd

State before:
case zero
absurd : zero ≠ 0
⊢ 0 < (val_bin_nat zero).snd
Tactic:
apply False.elim
State after:
case zero.h
absurd : zero ≠ 0
⊢ False

State before:
case zero.h
absurd : zero ≠ 0
⊢ False
Tactic:
apply absurd
State after:
case zero.h
absurd : zero ≠ 0
⊢ zero = 0

State before:
case zero.h
absurd : zero ≠ 0
⊢ zero = 0
Tactic:
rfl
State after:
no goals

State before:
case succ
x : ℕ
⊢ Nat.succ x ≠ 0 → 0 < (val_bin_nat (Nat.succ x)).snd
Tactic:
intro _
State after:
case succ
x : ℕ
a✝ : Nat.succ x ≠ 0
⊢ 0 < (val_bin_nat (Nat.succ x)).snd

State before:
case succ
x : ℕ
a✝ : Nat.succ x ≠ 0
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
Tactic:
exact odd_part_succ_pos x
State after:
no goals