diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSig.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index e53e627ec..5295aaec2 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -58,7 +58,7 @@ Module Type NType. Parameter spec_eq_bool: forall x y, if eq_bool x y then [x] = [y] else [x] <> [y]. - + Parameter succ : t -> t. Parameter spec_succ: forall n, [succ n] = [n] + 1. @@ -98,7 +98,7 @@ Module Type NType. Parameter spec_div_eucl: forall x y, 0 < [y] -> let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. - + Parameter div : t -> t -> t. Parameter spec_div: forall x y, 0 < [y] -> [div x y] = [x] / [y]. |