proposition: Theorem log_init : forall n, n < 2 -> log n == 0.
proof: Proof. intros n Hn. unfold log. rewrite strong_rec_fixpoint; auto with *. replace (n << 2) with true; auto with *. symmetry. now rewrite ltb_lt. Qed.
imports: Bool RelationPairs NStrongRec