Euler totient function is multiplicative!

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

diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma
index 5ebc08b6ce646d3e2b108cceab97967b4cad2c33..60bdbadc4c228ebc5019eea85d783fd70e00757d 100644 (file)
--- a/helm/matita/library/nat/count.ma
+++ b/helm/matita/library/nat/count.ma
@@ -123,7 +123,8 @@ theorem count_times:\forall n,m:nat.
 (count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
 intros.unfold count.
 rewrite < eq_map_iter_i_sigma.
-rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? (\lambda i.g (div i (S n)) (mod i (S n)))).
+rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? 
+           (\lambda i.g (div i (S n)) (mod i (S n)))).
 rewrite > eq_map_iter_i_sigma.
 rewrite > eq_sigma_sigma1.
 apply (trans_eq ? ?
@@ -131,8 +132,10 @@ apply (trans_eq ? ?
   sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O)).
 apply eq_sigma.intros.
 apply eq_sigma.intros.
-rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
-rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
+rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) 
+                                        ((i1*(S n) + i) \mod (S n)) i1 i).
+rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) 
+                                        ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.
 simplify.apply le_S_S.assumption.