(no commit message)

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

diff --git a/matita/library/nat/euler_theorem.ma b/matita/library/nat/euler_theorem.ma
index d58f7c2b06668c70c87fe20d67a4244b1f1738cd..d45c15dc3aa7b706ff8a1e9003cd0ed0e461d40e 100644 (file)
--- a/matita/library/nat/euler_theorem.ma
+++ b/matita/library/nat/euler_theorem.ma
@@ -17,7 +17,46 @@ set "baseuri" "cic:/matita/nat/euler_theorem".
 include "nat/map_iter_p.ma".
 include "nat/totient.ma".
 
+lemma gcd_n_n: \forall n.gcd n n = n.
+intro.elim n
+  [reflexivity
+  |apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S
+      |apply divides_gcd_n
+      ]
+    |apply divides_to_le
+      [apply lt_O_gcd.apply lt_O_S
+      |apply divides_d_gcd
+        [apply divides_n_n|apply divides_n_n]
+      ]
+    ]
+  ]
+qed.
+
+
+lemma count_card: \forall p.\forall n.
+p O = false \to count (S n) p = card n p.
+intros.elim n
+  [simplify.rewrite > H. reflexivity
+  |simplify.
+   rewrite < plus_n_O.
+   apply eq_f.assumption
+  ]
+qed.
+
+lemma count_card1: \forall p.\forall n.
+p O = false \to p n = false \to count n p = card n p.
+intros 3.apply (nat_case n)
+  [intro.simplify.rewrite > H. reflexivity
+  |intros.rewrite > (count_card ? ? H).
+   simplify.rewrite > H1.reflexivity
+  ]
+qed.
+ 
+
 (* a reformulation of totient using card insted of count *)
+
 lemma totient_card: \forall n. 
 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
 intro.apply (nat_case n)
@@ -38,8 +77,8 @@ intros 3.elim H
   [rewrite > pi_p_S.
    cut (eqb (gcd (S O) n) (S O) = true)
     [rewrite > Hcut.
-     change with ((gcd n (S O)) = (S O)).auto
-    |apply eq_to_eqb_true.auto
+     change with ((gcd n (S O)) = (S O)).autobatch
+    |apply eq_to_eqb_true.autobatch
     ]
   |rewrite > pi_p_S.
    apply eqb_elim
@@ -150,11 +189,11 @@ split
             |apply mod_O_to_divides
               [assumption
               |rewrite > distr_times_minus.
-               auto
+               autobatch
               ]
             ]
           ]
-        |auto
+        |autobatch
         ]
       ]
     |intro.assumption
@@ -175,11 +214,11 @@ split
             |apply mod_O_to_divides
               [assumption
               |rewrite > distr_times_minus.
-               auto
+               autobatch
               ]
             ]
           ]
-        |auto
+        |autobatch
         ]
       ]
     ]