diff options
Diffstat (limited to 'consecutive-fibonacci-numbers-are-coprime.lisp')
| -rw-r--r-- | consecutive-fibonacci-numbers-are-coprime.lisp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/consecutive-fibonacci-numbers-are-coprime.lisp b/consecutive-fibonacci-numbers-are-coprime.lisp index 482eb65..e9bc9e2 100644 --- a/consecutive-fibonacci-numbers-are-coprime.lisp +++ b/consecutive-fibonacci-numbers-are-coprime.lisp @@ -25,6 +25,12 @@ ((< n m) (gcd$ (- m n) n)) (t (gcd$ (- n m) m)))) +;; gcd$ の結果は正の整数である +(defthm posp-gcd$ + (implies (and (posp m) + (posp n)) + (posp (gcd$ m n)))) + ;; n と m が互いに素かどうかを調べる述語 (defmacro coprimep (n m) `(equal (gcd$ ,n ,m) 1)) |