Fixed sbralie

[GinoGiotto]

Requested by @benjub in #3571 (comment)

[benjub]

Does this MR restore the original proofs ? I don't understand: in #3571 (comment) @avekens noticed that the proof became longer, and now it seems that it becomes even longer instead of going back to the original ?

[GinoGiotto]

Does this MR restore the original proofs ? I don't understand: in #3571 (comment) @avekens noticed that the proof became longer, and now it seems that it becomes even longer instead of going back to the original ?

Ah, maybe I misinterpreted your request. What I did here is coupling DV(x,ps) and DV(y,ph) as you mentioned, but I still kept the new [ y / x ] notation. Restoring the original statement and proof would mean to go back to the [ x / y ] notation, which is against the request of issue #777 (sbralie is in the list of #777).

Also avekens accepted the new proof after I explained the reason of why it is longer: #3571 (comment) #3571 (comment)

EDIT: if you mean to restore the original proof only, I'm not sure that is possible because of the fact that I kept x = y in the hypothesis, so as you mentioned in #3571 this is a little more than a simple variable renaming.

EDIT2: same thing for ph and ps. I kept ph <-> ps in the hypothesis instead of switching into ps <-> ph and this caused an additional proof longening.

[tirix]

Good for me as-is.