theorem congruent_to_divides: ∀n,m,p:nat.O < p →
n ≅_{p} m → p ∣ (n - m).
#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
theorem congruent_to_divides: ∀n,m,p:nat.O < p →
n ≅_{p} m → p ∣ (n - m).
#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))