Submitted solution to problem 126

[ricostynha1]

Added solution to problem 126.

How it works:

• First, a sorting check is done
• Then we check if there are 3 elements equal in a row (if they are, we return false)
  (Mostly easy to do, but required some lemmas for concatenation).

The hard part was at the end to show that if a sequence is sorted, and no 3 in a row are equal, that implies that the count is necessarily equal to or less than 2 for each element:

This was done on the following:

• Created a lemma that proved that a sorted sequence can be subdivided into 3 parts, v1 + v2 + v3 = v, where v1 has elements smaller than w, v2 is equal to 2, and v3 is greater to w.
• Showing that the count could be made only on v2 of w, showing that the count is equal to the length of v2.
  And finally showing that by the property by contradiction, v2.len() must be smaller than or equal to 2.

[ One hard part to do was showing that the decomposition in v1 + v2 +v3 is possible; it required several lemmas, but it worked well ]

[parno]

It looks like this was more involved than expected, but you made it work. I added a few small comments. If you merge main into your branch, that will enable to CI to run on your PR.

[parno]

I think "decomposiiotn array in two 3" should be "decompose the array v into 3 parts:

[parno]

I suspect this precondition is unnecessary.

[ricostynha1]

changes were performed