n k : ℕ
h : MinFacHelper n k
this : 2 < minFac n
⊢ 1 < n
n k : ℕ
h : MinFacHelper n k
⊢ 1 < n
have : 2 < minFac n := h.1.trans_le h.2.2
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0

case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < minFac n
h : n > 0
⊢ 1 < n
n k : ℕ
h : MinFacHelper n k
this : 2 < minFac n
⊢ 1 < n
rcases eq_zero_or_pos n with rfl|h
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < minFac (succ 0)
h : succ 0 > 0
⊢ 1 < succ 0

case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < minFac n
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n
case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < minFac n
h : n > 0
⊢ 1 < n
rcases (succ_le_of_lt h).eq_or_lt with rfl|h
no goals
case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < minFac n
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n
exact h
no goals
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0
contradiction
no goals
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < minFac (succ 0)
h : succ 0 > 0
⊢ 1 < succ 0
contradiction