X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Flog.ma;h=6c7e159e416c0f4f1bc58bf9b5a3d501f479e7ac;hb=e90313fa853ba63f29416c2d0de40b13c913e567;hp=513c11e06ac446f3e2188bced5e1e95803f3c0cb;hpb=9b93455c674edb6e5d5d034df52666fedfe04bd4;p=helm.git

diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma
index 513c11e06..6c7e159e4 100644
--- a/matita/matita/lib/arithmetics/log.ma
+++ b/matita/matita/lib/arithmetics/log.ma
@@ -10,8 +10,8 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/exp.ma".
-include "arithmetics/minimization.ma".
 include "arithmetics/div_and_mod.ma".
+include "arithmetics/minimization.ma".
 
 definition log ≝ λp,n.
   max n (λx.leb (exp p x) n).
@@ -67,8 +67,6 @@ theorem le_log_n_n: ∀p,n. 1 < p → log p n ≤ n.
 #p #n #lt1p cases n [@le_n |#m @lt_to_le @lt_log_n_n //]
 qed.
 
-axiom daemon : ∀P:Prop.P.
-
 theorem lt_exp_log: ∀p,n. 1 < p → n < exp p (S (log p n)).
 #p #n #lt1p cases n
   [normalize <plus_n_O @lt_to_le // 
@@ -142,7 +140,7 @@ theorem log_exp: ∀p,n,m. 1 < p → O < m →
   |#i #Hi #Hm @lt_to_leb_false
    @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
     [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
-    |<exp_plus_times @le_exp [@lt_to_le // |<plus_n_Sm //]
+    |<exp_plus_times @le_exp [@lt_to_le // | //]
     ]
   ]
 qed.