#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
>commutative_times >(div_mod n p) in ⊢ (??%?)
>(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
>commutative_times >(div_mod n p) in ⊢ (??%?)
>(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))