theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
gcd p n = 1 → p ∣ (n*m) → p ∣ m.
#p #m #n #posn #gcd1 * #c #nm
theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
gcd p n = 1 → p ∣ (n*m) → p ∣ m.
#p #m #n #posn #gcd1 * #c #nm