->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/
+>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/