proposition: Theorem log_step : forall n, 2 <= n -> log n == S (log (half n)).
proof: Proof. intros n Hn. unfold log. rewrite strong_rec_fixpoint; auto with *. replace (n << 2) with false; auto with *. symmetry. rewrite <- not_true_iff_false, ltb_lt, nlt_ge; auto. Qed.
imports: Bool RelationPairs NStrongRec