diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-07-25 19:01:51 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-07-26 14:47:07 +0900 |
| commit | dbe9a9451945db5fa3ce8c308bacd478b2a6d315 (patch) | |
| tree | 968e61f713c0d1c00c3b93e8dfbc78d5d2c880ab /consecutive-fibonacci-numbers-are-coprime.lisp | |
| parent | f128e3939d1b547a3a408529b8698d08ebcaf6d7 (diff) | |
consecutive-fibonacci-numbers-are-coprime: gcd$ の結果が正の整数になる性質を証明した
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)) |