proposition: Theorem spec_shiftl_aux_body: forall n x p cont, 2^ Zpos p <= [head0 x] -> (forall x, 2 ^ (Zpos p + 1) <= [head0 x]-> [cont x n] = [x] * 2 ^ [n]) -> [shiftl_aux_body cont x n] = [x] * 2 ^ [n].
proof: Proof. intros n x p cont H1 H2; unfold shiftl_aux_body. rewrite spec_compare; case Z.compare_spec; intros H. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite H2. rewrite spec_double_size; auto. rewrite Z.add_comm; rewrite Zpower_exp; auto with zarith. apply Z.le_trans with (2 := spec_double_size_head0 x). rewrite Z.pow_1_r; apply Z.mul_le_mono_nonneg_l; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen