sets cover Nat

Stream: general

[Matthew Pocock]

I have a series of expressions. For example: 3a, 3b+1, 3c+2. They are always simple linear functions in Nat with Nat multiplier and constant, but aren't always this kind of obvious series. I want to prove that these collectively generate the whole of Nat, possibly with overlap. I don't always have 3 linear functions, but so far I think it is always a small number of cases. Is there some strategy I should be reaching for to automate this, or do I write it down as something like: \all n : Nat, n = 3a or n = 3a+1 or n = 3a+2? I could use each expression to indue a set, take their union and prove that it is or it contains Nat perhaps?

[Yaël Dillies]

You're doing covering congruences, right? Then you should prove that every element mod the lcm of the multipliers is hit by one of the functions.