proposition: Lemma log_good_step : forall n h1 h2, (forall m, m < n -> h1 m == h2 m) -> (if n << 2 then 0 else S (h1 (half n))) == (if n << 2 then 0 else S (h2 (half n))).
proof: Proof. intros n h1 h2 E. destruct (n<<2) eqn:H. - auto with *. - f_equiv. apply E, half_decrease. rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. order'. Qed.
imports: Bool RelationPairs NStrongRec