Euler totient function is multiplicative!

[helm.git] / helm / matita / library / nat / primes.ma

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 74fd74e7455de4b999461b2944efcd952fe96ad1..452adc89c9788ac726cdd661ffb83294865353bd 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -150,6 +150,23 @@ assumption.
 apply (decidable_le n m).
 qed.
 
+theorem antisymmetric_divides: antisymmetric nat divides.
+simplify.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.
+
 (* 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).