Hi everyone,

My goal is the following:

I can use an existing theorem to show there exist odd positive integers x, y and z such that n = x^2+y^2+z^2 if n mod 8 = 3. However, I'd like to assume without loss of generality that x >= y >= z. This assumption is not given in the original theorem, I wonder if there is any efficient way to do this.

Thank you so much for the help!

The easiest way I see is to rewrite it as `n = sum_list (map (λx. x^2) [x,y,z])`

and then show that this is the same as `sum_list (map (λx. x^2) (sort [x,y,z]))`

and then obtain values `a`

, `b`

, `c`

such that `[a,b,c] = sort [x,y,z]`

.

Each of those steps should be doable with a few suitable library lemmas and help from sledgehammer. But depending on how much experience you have with Isabelle it could still be a bit tricky, so feel free to ask if you are stuck with any particular step.

(might be sensible to go through multisets to justify that the two sets are the same)

alternatively you could of course just do a case distinction; that should also work

That is, proving the stronger version of the theorem from the weaker one with a `by (cases "x ≤ y"; cases "y ≤ z"; cases "x ≤ z") (auto simp: algebra_simps)`

or something like that (not sure if that's enough).

That works! Thank you so much :)

Last updated: Dec 07 2023 at 20:16 UTC