[GOAL]
⊢ SuccOrder (Fin 0)
[PROOFSTEP]
constructor
[GOAL]
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a
[PROOFSTEP]
assumption
[GOAL]
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a
[PROOFSTEP]
intro a
[GOAL]
case le_succ
a : Fin 0
⊢ a ≤ ?succ a
[PROOFSTEP]
exact elim0 a
[GOAL]
case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a
[PROOFSTEP]
assumption
[GOAL]
case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a
[PROOFSTEP]
intro a
[GOAL]
case max_of_succ_le
a : Fin 0
⊢ ?succ a ≤ a → IsMax a
[PROOFSTEP]
exact elim0 a
[GOAL]
case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
intro a
[GOAL]
case succ_le_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
exact elim0 a
[GOAL]
case le_of_lt_succ
⊢ ∀ {a b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_of_lt_succ
⊢ ∀ {a b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case le_of_lt_succ
⊢ ∀ {a b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
intro a
[GOAL]
case le_of_lt_succ
a : Fin 0
⊢ ∀ {b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
exact elim0 a
[GOAL]
case succ
⊢ Fin 0 → Fin 0
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case succ
⊢ Fin 0 → Fin 0
[PROOFSTEP]
assumption
[GOAL]
case succ
⊢ Fin 0 → Fin 0
[PROOFSTEP]
intro a
[GOAL]
case succ
a : Fin 0
⊢ Fin 0
[PROOFSTEP]
exact elim0 a
[GOAL]
n : ℕ
⊢ ∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
[PROOFSTEP]
intro a ha b
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : ¬IsMax a
b : Fin (n + 1)
⊢ a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
[PROOFSTEP]
rw [isMax_iff_eq_top, eq_top_iff, not_le, top_eq_last] at ha 
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMax a
ha : a < last n
b : Fin (n + 1)
⊢ a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMax a
ha : a < last n
b : Fin (n + 1)
⊢ a < b ↔ (if a < last n then a + 1 else a) ≤ b
[PROOFSTEP]
rw [if_pos ha, lt_iff_val_lt_val, le_iff_val_le_val, val_add_one_of_lt ha]
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMax a
ha : a < last n
b : Fin (n + 1)
⊢ ↑a < ↑b ↔ ↑a + 1 ≤ ↑b
[PROOFSTEP]
exact Nat.lt_iff_add_one_le
[GOAL]
n : ℕ
⊢ ∀ (a : Fin (n + 1)), IsMax a → (fun i => if i < last n then i + 1 else i) a = a
[PROOFSTEP]
intro a ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : IsMax a
⊢ (fun i => if i < last n then i + 1 else i) a = a
[PROOFSTEP]
rw [isMax_iff_eq_top, top_eq_last] at ha 
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMax a
ha : a = last n
⊢ (fun i => if i < last n then i + 1 else i) a = a
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMax a
ha : a = last n
⊢ (if a < last n then a + 1 else a) = a
[PROOFSTEP]
rw [if_neg ha.not_lt]
[GOAL]
⊢ PredOrder (Fin 0)
[PROOFSTEP]
constructor
[GOAL]
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a
[PROOFSTEP]
assumption
[GOAL]
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a
[PROOFSTEP]
intro a
[GOAL]
case pred_le
a : Fin 0
⊢ ?pred a ≤ a
[PROOFSTEP]
exact elim0 a
[GOAL]
case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a
[PROOFSTEP]
assumption
[GOAL]
case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a
[PROOFSTEP]
intro a
[GOAL]
case min_of_le_pred
a : Fin 0
⊢ a ≤ ?pred a → IsMin a
[PROOFSTEP]
exact elim0 a
[GOAL]
case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
assumption
[GOAL]
case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
intro a
[GOAL]
case le_pred_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
exact elim0 a
[GOAL]
case le_of_pred_lt
⊢ ∀ {a b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_of_pred_lt
⊢ ∀ {a b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case le_of_pred_lt
⊢ ∀ {a b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
intro a
[GOAL]
case le_of_pred_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
exact elim0 a
[GOAL]
case pred
⊢ Fin 0 → Fin 0
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case pred
⊢ Fin 0 → Fin 0
[PROOFSTEP]
assumption
[GOAL]
case pred
⊢ Fin 0 → Fin 0
[PROOFSTEP]
intro a
[GOAL]
case pred
a : Fin 0
⊢ Fin 0
[PROOFSTEP]
exact elim0 a
[GOAL]
n : ℕ
⊢ ∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
[PROOFSTEP]
intro a ha b
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : ¬IsMin a
b : Fin (n + 1)
⊢ b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
[PROOFSTEP]
rw [isMin_iff_eq_bot, eq_bot_iff, not_le, bot_eq_zero] at ha 
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ (b ≤ if a = 0 then 0 else a - 1) ↔ b < a
[PROOFSTEP]
rw [if_neg ha.ne', lt_iff_val_lt_val, le_iff_val_le_val, coe_sub_one, if_neg ha.ne', le_tsub_iff_right, Iff.comm]
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ ↑b < ↑a ↔ ↑b + 1 ≤ ↑a
n : ℕ a : Fin (n + 1) ha✝ : ¬IsMin a ha : 0 < a b : Fin (n + 1) ⊢ 1 ≤ ↑a
[PROOFSTEP]
exact Nat.lt_iff_add_one_le
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ 1 ≤ ↑a
[PROOFSTEP]
exact ha
[GOAL]
n : ℕ
⊢ ∀ (a : Fin (n + 1)), IsMin a → (fun x => if x = 0 then 0 else x - 1) a = a
[PROOFSTEP]
intro a ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : IsMin a
⊢ (fun x => if x = 0 then 0 else x - 1) a = a
[PROOFSTEP]
rw [isMin_iff_eq_bot, bot_eq_zero] at ha 
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMin a
ha : a = 0
⊢ (fun x => if x = 0 then 0 else x - 1) a = a
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMin a
ha : a = 0
⊢ (if a = 0 then 0 else a - 1) = a
[PROOFSTEP]
rwa [if_pos ha, eq_comm]
