proposition: Lemma log2_iter_spec : forall k p q r, 2^(S p) = q + S r -> r < 2^p -> let s := log2_iter k p q r in 2^s <= k + q < 2^(S s).
proof: Proof. intro k; induction k as [|k IHk]. - intros p q r EQ LT. simpl log2_iter; cbv zeta. split. + rewrite add_0_l, (add_le_mono_l _ _ (2^p)). simpl pow in EQ. rewrite add_0_r in EQ; rewrite EQ, add_comm. apply add_le_mono_r, LT. + rewrite EQ, add_comm. apply add_lt_mono_l. apply lt_succ_r, le_0_l. - intros p q r EQ LT. destruct r as [|r]. + rewrite add_succ_r, add_0_r in EQ. rewrite add_succ_l, <- add_succ_r. apply IHk. * rewrite <- EQ. remember (S p) as p'; simpl. now rewrite add_0_r. * rewrite EQ; constructor. + rewrite add_succ_l, <- add_succ_r. apply IHk. * now rewrite add_succ_l, <- add_succ_r. * apply le_lt_trans with (S r); trivial. do 2 constructor. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass