proposition: Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x).
proof: Proof. intros. destruct x as [p|p]; simpl. apply NN.spec_log2. rewrite NN.spec_0. destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. rewrite Z.log2_nonpos; auto with zarith. now rewrite <- EQ. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig