diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_extras.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 626b4109..51856d9e 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -162,10 +162,12 @@ Require DecimalString. Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). -Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * size ÷ 8). +Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * (8 * size ÷ 8) ÷ 8). intros. rewrite Z.mul_comm. rewrite Z.quot_mul; auto with zarith. +rewrite Z.mul_comm with (m := size). +rewrite Z.quot_mul; auto with zarith. Qed. Hint Resolve MEMr_wrapper_lemma : sail. |