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).
#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 //
|#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.