proposition: Theorem spec_unsafe_shiftl_aux : forall x p K, 0 <= K -> [x] < 2^K -> [p] + K <= Zpos (digits x) -> [unsafe_shiftl x p] = [x] * 2 ^ [p].
proof: Proof. intros x p. rewrite unsafe_shiftl_fold. rewrite digits_level. apply spec_same_level_dep. intros n m z z' r LE H K HK H1 H2. apply (H K); auto. transitivity (Zpos (ZnZ.digits (dom_op n))); auto. apply digits_dom_op_incr; auto. clear x p. intros n x p K HK Hx Hp. simpl. rewrite spec_reduce. destruct (ZnZ.spec_to_Z x). destruct (ZnZ.spec_to_Z p). rewrite ZnZ.spec_add_mul_div by lia. rewrite ZnZ.spec_0, Zdiv_0_l, Z.add_0_r. apply Zmod_small. unfold base. split; auto with zarith. rewrite Z.mul_comm. apply Z.lt_le_trans with (2^(ZnZ.to_Z p + K)). rewrite Zpower_exp; auto with zarith. apply Z.mul_lt_mono_pos_l; auto with zarith. apply Z.pow_le_mono_r; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen