From dbe9a9451945db5fa3ce8c308bacd478b2a6d315 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 25 Jul 2021 19:01:51 +0900
Subject: consecutive-fibonacci-numbers-are-coprime: gcd$
 の結果が正の整数になる性質を証明した
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 consecutive-fibonacci-numbers-are-coprime.lisp | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'consecutive-fibonacci-numbers-are-coprime.lisp')

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))
-- 
cgit v1.2.3