Unnecessary assumption in sorted_take

[ybertot]

Hello,
in CoqEAL0.1, sorted_take (from ssrcomplements.v) had no transitivity assumption. In CoqEAL1.0.5, such an assumption exists. It may turn out be a problem one day.

[proux01]

Indeed, this lemma should be removed as it is now in MC https://github.com/math-comp/math-comp/blob/14097e37cb3b0590ef5d91809acf4fed0fb22f1a/mathcomp/ssreflect/path.v#L369

[ybertot]

I do not understand. sorted_take does not occur in the current master branch of math-comp. What is the commit that @proux01 mentions attached to?

[proux01]

It's take_sorted : https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/path.v#L369

[ybertot]

thks, I did not pay enough attention.

[proux01]

I'd rather keep this open to remember to do the change once MC 1.13 is out.