proposition: Lemma mod_log2 : forall a b r:positive, a mod b = Npos r -> b <= a -> log2 r + 1 <= log2 a.
proof: Proof. intros; cut (log2 (xO r) <= log2 a). simpl;zsimpl;trivial. apply log2_Zle. replace (Zpos (xO r)) with (2 * r)%Z;trivial. generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;rewrite H. rewrite Zmult_comm;intros [H1 H2];apply mod_le_2r with b (fst (a/b));trivial. Qed.
imports: ZArith Lia ZCmisc