X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Flog.ma;h=bbd65be967edac94f57b849d89632f1dca0a6895;hb=225887a9f23aac79d4cca907da026917b7df04dc;hp=733720ce340a3375f6b92e8fff00359d08a3ade8;hpb=29c979302cf398410bf6f10c11b146ebe42bd54a;p=helm.git

diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma
index 733720ce3..bbd65be96 100644
--- a/matita/matita/lib/arithmetics/log.ma
+++ b/matita/matita/lib/arithmetics/log.ma
@@ -140,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.