->commutative_times {⊢ (? ? %)} <div_mod
->(div_mod m q) {⊢ (? ? (? % ?))} >(div_mod n q) {⊢ (? ? (? ? %))}
->commutative_plus {⊢ (? ? (? % ?))} >associative_plus {⊢ (? ? %)}
-<associative_plus {⊢ (? ? (? ? %))} (applyS monotonic_le_plus_l) /2/
+>commutative_times in ⊢ (? ? %); <div_mod
+>(div_mod m q) in ⊢ (? ? (? % ?)); >(div_mod n q) in ⊢ (? ? (? ? %));
+>commutative_plus in ⊢ (? ? (? % ?)); >associative_plus in ⊢ (? ? %);
+<associative_plus in ⊢ (? ? (? ? %)); (applyS monotonic_le_plus_l) /2/