better name for a theorem

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 515388917482d366cffd19c7dc808bf4424a2d87..43fe7f649ba4ac93223e4f213fa77369cd7a582a 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -41,7 +41,7 @@ rewrite < plus_n_O.
 rewrite > div_times.apply sym_times.
 qed.
 
-theorem div_mod_spec_to_div :
+theorem div_mod_spec_to_divides :
 \forall n,m,p. div_mod_spec m n p O \to n \divides m.
 intros.elim H.
 apply witness n m p.
@@ -105,14 +105,17 @@ rewrite > sym_times n2 m.apply assoc_times.
 apply sym_eq. apply assoc_times.
 qed.
 
-theorem transitive_divides: \forall n,m,p. 
-n \divides m \to m \divides p \to n \divides p.
+theorem transitive_divides: transitive ? divides.
+unfold.
 intros.
-elim H.elim H1. apply witness n p (n2*n1).
+elim H.elim H1. apply witness x z (n2*n).
 rewrite > H3.rewrite > H2.
 apply assoc_times.
 qed.
 
+variant trans_divides: \forall n,m,p. 
+ n \divides m \to m \divides p \to n \divides p \def transitive_divides.
+
 (* divides le *)
 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
 intros. elim H1.rewrite > H2.cut O < n2.