diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/Nbasic.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 161f523ca..e8a9940bd 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -320,6 +320,7 @@ Section CompareRec. Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos). + Declare Equivalent Keys compare0_mn compare0_m. Lemma spec_compare0_mn: forall n x, compare0_mn n x = (0 ?= double_to_Z n x). |