Commit 2023-09-02 20:42 0135e4c1

feat: Elements less than some value of a sorted tuple are at the beginning of the tuple. (#6728) For a sorted (monotone) tuple containing n elements with exactly r elements less than or equal some value, all these elements are at the first r locations of the tuple. Proofs by @Ruben-VandeVelde , @ericrbg @eric-wieser see Zulip Thread