->associative_times in ⊢ (???(?(??%)?))
->commutative_times in ⊢ (???(?(??(??%))?))
-<associative_times in ⊢ (???(?(??%)?))
->(div_times_times ?? (n - k)) in ⊢ (???(??%))
+>associative_times {⊢ (???(?(??%)?))}
+>commutative_times {⊢ (???(?(??(??%))?))}
+<associative_times {⊢ (???(?(??%)?))}
+>(div_times_times ?? (n - k)) {⊢ (???(??%))}