<commutative_plus <plus_minus
[@(eq_times_plus_to_congruent … posm) //
|applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) //
<commutative_plus <plus_minus
[@(eq_times_plus_to_congruent … posm) //
|applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) //