diff options
Diffstat (limited to 'kvx/FPDivision64.v')
| -rw-r--r-- | kvx/FPDivision64.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 0d11c3cb..a53169b8 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1366,7 +1366,9 @@ Proof. with (-(a' - a' / b' * b')+b')%Z by ring. rewrite <- MOD. rewrite Int64.signed_repr; cycle 1. - { admit. + { change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + lia. } rewrite zlt_true by lia. ring. @@ -1376,8 +1378,10 @@ Proof. replace (a' / b' * b' - a')%Z with (-(a' - a' / b' * b'))%Z by ring. rewrite <- MOD. rewrite Int64.signed_repr ; cycle 1. - { admit. + { change Int64.min_signed with (-9223372036854775808)%Z in *. + change Int64.max_signed with (9223372036854775807)%Z in *. + lia. } rewrite zlt_false by lia. reflexivity. -Admitted. +Qed. |