∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M]
  [inst_3 : LocallyFiniteOrder M] [ExistsAddOfLE M] (a b : M),
  0 ≤ a → 0 ≤ b → (Finset.Ico 0 a).card + (Finset.Ico 0 b).card = (Finset.Ico 0 (a + b)).card