## Stream: Beginner Questions

### Topic: Without loss of generality

#### Chris_Y (Jun 27 2023 at 14:35):

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!

#### Manuel Eberl (Jun 27 2023 at 15:09):

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]`.

#### Manuel Eberl (Jun 27 2023 at 15:10):

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.

#### Manuel Eberl (Jun 27 2023 at 15:10):

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

#### Manuel Eberl (Jun 27 2023 at 15:11):

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

#### Manuel Eberl (Jun 27 2023 at 15:12):

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).

#### Chris_Y (Jun 27 2023 at 16:38):

That works! Thank you so much :)

Last updated: Sep 09 2024 at 08:25 UTC