F : Type ?u.152613
α : Type ?u.152616
β : Type ?u.152619
𝕜 : Type ?u.152622
E : Type ?u.152625
s : Finset ℕ
k n M N : ℕ
⊢ ↑addRothNumber (range (M + N)) ≤ ↑addRothNumber (range M) + ↑addRothNumber (range N)
F : Type ?u.152613
α : Type ?u.152616
β : Type ?u.152619
𝕜 : Type ?u.152622
E : Type ?u.152625
s : Finset ℕ
k n M N : ℕ
⊢ ↑rothNumberNat (M + N) ≤ ↑rothNumberNat M + ↑rothNumberNat N
simp_rw [rothNumberNat_def]
F : Type ?u.152613
α : Type ?u.152616
β : Type ?u.152619
𝕜 : Type ?u.152622
E : Type ?u.152625
s : Finset ℕ
k n M N : ℕ
⊢ ↑addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    ↑addRothNumber (range M) + ↑addRothNumber (map (addLeftEmbedding M) (range N))
F : Type ?u.152613
α : Type ?u.152616
β : Type ?u.152619
𝕜 : Type ?u.152622
E : Type ?u.152625
s : Finset ℕ
k n M N : ℕ
⊢ ↑addRothNumber (range (M + N)) ≤ ↑addRothNumber (range M) + ↑addRothNumber (range N)
rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]
no goals
F : Type ?u.152613
α : Type ?u.152616
β : Type ?u.152619
𝕜 : Type ?u.152622
E : Type ?u.152625
s : Finset ℕ
k n M N : ℕ
⊢ ↑addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    ↑addRothNumber (range M) + ↑addRothNumber (map (addLeftEmbedding M) (range N))
exact addRothNumber_union_le _ _