Доказательство рекурсивной функции Coq

у меня проблема с доказательством в Coq.
Нужно написать рекурсивную функцию и ее спецификацию, а затем доказать, что написанная функция удовлетворяет спецификации.
Вспомогательные факты следует оформить как леммы. Например, так можно поступить с шагом индукции, чтобы основное доказательство было компактным.
Проект:
Целочисленным логарифмом числа n по основанию b называется максимальное число p, такое что b^p <= n. Требуется написать функцию log b n, вычисляющую целочисленный логарифм. Можно использовать функцию возведения в степень, которая обозначается x^y или pow x y.
Вот что примерно получилось:

Require Import Arith.
Require Import Omega.
Require Import Bool.
Import Nat Peano.



Hint Resolve ltb_spec0 leb_spec0 eqb_spec : bdestruct.

Ltac bdestr X H :=
  let e := fresh "e" in
   evar (e : Prop);
   assert (H : reflect e X); subst e;
    [eauto with bdestruct
    | destruct H as [H | H];
       [ | try first [apply nlt_ge in H | apply nle_gt in H]]].

(* Boolean destruct *)

Tactic Notation "bdestruct" constr(X) := let H := fresh in bdestr X H.

Tactic Notation "bdestruct" constr(X) "as" ident(H) := bdestr X H.


Section log.

Fixpoint log_help (a b c : nat) : nat:=
match c with
| 0 => 0
| S k => if (a^k <=? b) then k else log_help a b k
end.

Definition my_log (a b : nat) : nat:= log_help a b (a*b).
(* В качестве верхней грани для логарифма используем a*b  *)


(* Тестовые вызовы функции *)
Compute my_log 1 1.
Compute my_log 2 2.
Compute my_log 2 4.
Compute my_log 2 8.
Compute my_log 3 3.

Lemma log_help_def : forall b n p, b^p <= n -> log_help b n (S p) = p.
Proof.
intros b n p H. simpl. destruct (b ^ p <=? n) eqn:H1. 
auto. 
apply (leb_correct (b^p) n) in H. rewrite H in H1. discriminate H1.
Qed.


Lemma log_help_def0 : forall b n , log_help b n 0 = 0.
Proof.
intros b n. simpl. auto.
Qed.


Lemma log_help_lemma : forall b n p , (b^(log_help b n p)<=n <-> 
          b^(S (log_help b n p)) > n).
Proof.
split; intro H.
+ simpl.
  induction p as [| p IH].
  * simpl. simpl in H. 
Admitted.

Theorem my_log_spec : forall b n , b^my_log b n <=n <-> 
          b^(S (my_log b n)) > n.
Proof.
split; intro H.
+ simpl.
Admitted.

Не понимаю, как двигаться дальше. Есть ли какие-нибудь варианты решения проблемы?