Still porting chebyshev

[helm.git] / matita / matita / lib / arithmetics / log.ma

diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma
index 513c11e06ac446f3e2188bced5e1e95803f3c0cb..733720ce340a3375f6b92e8fff00359d08a3ade8 100644 (file)
--- a/matita/matita/lib/arithmetics/log.ma
+++ b/matita/matita/lib/arithmetics/log.ma
@@ -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 //