From 2c22c8fe144cbce796168ffd9843a87f06dcfa76 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 26 Sep 2005 08:57:20 +0000 Subject: [PATCH] better name for a theorem --- helm/matita/library/nat/primes.ma | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 515388917..43fe7f649 100644 --- 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. -- 2.39.2