equal
deleted
inserted
replaced
364 have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2" |
364 have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2" |
365 by simp |
365 by simp |
366 also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)" |
366 also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)" |
367 proof cases |
367 proof cases |
368 assume "0 \<le> u x" then show ?thesis |
368 assume "0 \<le> u x" then show ?thesis |
369 by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg) |
369 by (intro le_mult_natfloor) |
370 next |
370 next |
371 assume "\<not> 0 \<le> u x" then show ?thesis |
371 assume "\<not> 0 \<le> u x" then show ?thesis |
372 by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg) |
372 by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg) |
373 qed |
373 qed |
374 also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)" |
374 also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)" |