α : Type ?u.45406
β : Type ?u.45409
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l
α : Type ?u.45406
β : Type ?u.45409
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
⊢ raise (lower (m :: l) n) n = m :: l
have : n ≤ m := List.rel_of_sorted_cons h _ (l.mem_cons_self _)
no goals
α : Type ?u.45406
β : Type ?u.45409
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l
simp [raise, lower, tsub_add_cancel_of_le this, raise_lower h.of_cons]