theorem divides_plus: \forall n,p,q:nat.
n \divides p \to n \divides q \to n \divides p+q.
intros.
theorem divides_plus: \forall n,p,q:nat.
n \divides p \to n \divides q \to n \divides p+q.
intros.
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
qed.
theorem divides_minus: \forall n,p,q:nat.
divides n p \to divides n q \to divides n (p-q).
intros.
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
qed.
theorem divides_minus: \forall n,p,q:nat.
divides n p \to divides n q \to divides n (p-q).
intros.
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
qed.
theorem divides_times: \forall n,m,p,q:nat.
n \divides p \to m \divides q \to n*m \divides p*q.
intros.
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
qed.
theorem divides_times: \forall n,m,p,q:nat.
n \divides p \to m \divides q \to n*m \divides p*q.
intros.
theorem antisymmetric_divides: antisymmetric nat divides.
unfold antisymmetric.intros.elim H. elim H1.
theorem antisymmetric_divides: antisymmetric nat divides.
unfold antisymmetric.intros.elim H. elim H1.