theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
p \divides (m \mod n) \to p \divides n \to p \divides m.
intros.elim H1.elim H2.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
p \divides (m \mod n) \to p \divides n \to p \divides m.
intros.elim H1.elim H2.