Commit 2021-10-23 14:30 e1c0dbc8

feat(set_theory/cardinal): add add_le_omega (#9887)

• simplify c₁ + c₂ ≤ ω to c₁ ≤ ω ∧ c₂ ≤ ω;
• simplify ω + ω to ω;
• simplify #s ≤ ω to s.countable;
• simplify (s ∪ t).countable and (insert a s).countable. Motivated by lemmas from flypitch.