+variant trans_divides: \forall n,m,p.
+ n \divides m \to m \divides p \to n \divides p \def transitive_divides.
+
+theorem eq_mod_to_divides:\forall n,m,p. O< p \to
+mod n p = mod m p \to divides p (n-m).
+intros.
+cut (n \le m \or \not n \le m).
+elim Hcut.
+cut (n-m=O).
+rewrite > Hcut1.
+apply (witness p O O).
+apply times_n_O.
+apply eq_minus_n_m_O.
+assumption.
+apply (witness p (n-m) ((div n p)-(div m p))).
+rewrite > distr_times_minus.
+rewrite > sym_times.
+rewrite > (sym_times p).
+cut ((div n p)*p = n - (mod n p)).
+rewrite > Hcut1.
+rewrite > eq_minus_minus_minus_plus.
+rewrite > sym_plus.
+rewrite > H1.
+rewrite < div_mod.reflexivity.
+assumption.
+apply sym_eq.
+apply plus_to_minus.
+rewrite > sym_plus.
+apply div_mod.
+assumption.
+apply (decidable_le n m).
+qed.
+
+theorem antisymmetric_divides: antisymmetric nat divides.
+unfold antisymmetric.intros.elim H. elim H1.
+apply (nat_case1 n2).intro.
+rewrite > H3.rewrite > H2.rewrite > H4.
+rewrite < times_n_O.reflexivity.
+intros.
+apply (nat_case1 n).intro.
+rewrite > H2.rewrite > H3.rewrite > H5.
+rewrite < times_n_O.reflexivity.
+intros.
+apply antisymmetric_le.
+rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
+rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
+qed.
+