(prefix,left,right,suffix) ← match_assoc unif l r finds the longest prefix and suffix common to l and r and returns them along with the differences

tactic-facing function, similar to interactive.tactic.generalize with the exception that meta variables

• mono applies a monotonicity rule.
• mono* applies monotonicity rules repetitively.
• mono with x ≤ y or mono with [0 ≤ x,0 ≤ y] creates an assertion for the listed propositions. Those help to select the right monotonicity rule.
• mono left or mono right is useful when proving strict orderings: for x + y < w + z could be broken down into either
  • left: x ≤ w and y < z or
  • right: x < w and y ≤ z

transforms a goal of the form f x ≼ f y into x ≤ y using lemmas marked as monotonic.

Special care is taken when f is the repeated application of an associative operator and if the operator is commutative

(repeat_until_or_at_most n t u): repeat tactic t at most n times or until u succeeds

ac_mono reduces the f x ⊑ f y, for some relation ⊑ and a monotonic function f to x ≺ y.

ac_mono* unwraps monotonic functions until it can't.

ac_mono^k, for some literal number k applies monotonicity k times.

ac_mono h, with h a hypothesis, unwraps monotonic functions and uses h to solve the remaining goal. Can be combined with * or ^k: ac_mono* h

ac_mono : p asserts p and uses it to discharge the goal result unwrapping a series of monotonic functions. Can be combined with * or ^k: ac_mono* : p

In the case where f is an associative or commutative operator, ac_mono will consider any possible permutation of its arguments and use the one the minimizes the difference between the left-hand side and the right-hand side.

TODO(Simon): with ac_mono h and ac_mono : p split the remaining gaol if the provided rule does not solve it completely.