proposition: Theorem spec_unsafe_shiftl: forall x p, [p] <= [head0 x] -> [unsafe_shiftl x p] = [x] * 2 ^ [p].
proof: Proof. intros. destruct (Z.eq_dec [x] 0) as [EQ|NEQ]. apply spec_unsafe_shiftl_aux with 0. auto with zarith. now rewrite EQ. rewrite spec_head00 in *; auto with zarith. apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith. generalize (spec_pos (log2 x)); auto with zarith. destruct (spec_log2_pos x); auto with zarith. rewrite log2_digits_head0; auto with zarith. generalize (spec_pos x); auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen