Theorem: PFin2.toNat_lt (Qpf/MathlibPort/Fin2.lean)

State before:
n : ℕ
i : PFin2 n
⊢ toNat i < n
Tactic:
induction i
State after:
case fz
n n✝ : ℕ
⊢ toNat fz < succ n✝

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : toNat a✝ < n✝
⊢ toNat (fs a✝) < succ n✝

State before:
n n✝ : ℕ
⊢ toNat fz < succ n✝
Tactic:
case fz       => apply succ_pos
State after:
no goals

State before:
n n✝ : ℕ
a✝ : PFin2 n✝
ih : toNat a✝ < n✝
⊢ toNat (fs a✝) < succ n✝
Tactic:
case fs _ ih  => apply lt_succ_of_le ih
State after:
no goals

State before:
n n✝ : ℕ
⊢ toNat fz < succ n✝
Tactic:
apply succ_pos
State after:
no goals

State before:
n n✝ : ℕ
a✝ : PFin2 n✝
ih : toNat a✝ < n✝
⊢ toNat (fs a✝) < succ n✝
Tactic:
apply lt_succ_of_le ih
State after:
no goals