|#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 //]
|#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 //]