notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
notation > "s 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
notation > "s 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
interpretation "Ordered set strict decreasing" 'strictly_decreasing s =