diff options
Diffstat (limited to 'flocq/Core/Fcore_digits.v')
| -rw-r--r-- | flocq/Core/Fcore_digits.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index d40c1a09..53743035 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -853,7 +853,7 @@ Proof. intros n Zn. rewrite <- (Zdigits_abs n). assert (Hn: (0 < Zabs n)%Z). -destruct n ; try easy. +destruct n ; [|easy|easy]. now elim Zn. destruct (Zabs n) as [|p|p] ; try easy ; clear. simpl. |