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