-@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
- [@eq_f2 //
- |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
- (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
- >distributive_times_plus >distributive_times_plus_r
- >distributive_times_plus_r <associative_plus @eq_f2 //
+@(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
+@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
+ (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
+ [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d)
+ [#a #b #c #d >(distributive_times_plus_r (c+d) a b)
+ >(distributive_times_plus a c d)
+ >(distributive_times_plus b c d) //] #Hcut
+ @Hcut
+ |@eq_f2
+ [<associative_times >(associative_times (n/p) p (m \mod p))
+ >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
+ >distributive_times_plus_r //
+ |%
+ ]