diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 5037d617b..21e786a17 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -87,9 +87,9 @@ Save. either [(log_sup p)=(log_inf p)+1] *) Theorem log_sup_log_inf : (p:positive) - either (POS p)=(two_p (log_inf p)) - and_then (POS p)=(two_p (log_sup p)) - or_else ` (log_sup p)=(Zs (log_inf p))`. + IF (POS p)=(two_p (log_inf p)) + then (POS p)=(two_p (log_sup p)) + else ` (log_sup p)=(Zs (log_inf p))`. Induction p; Intros; [ Elim H; Right; Simpl; |