# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615616454 -32400
# Node ID 6cd9d874cc552e86b257d3a31f0098ff8dd338b2
# Parent  1c43d0713dfc584d730b433d23ea25e76ff19a26
...

diff -r 1c43d0713dfc -r 6cd9d874cc55 agda/prime.agda
--- a/agda/prime.agda	Sat Mar 13 15:12:18 2021 +0900
+++ b/agda/prime.agda	Sat Mar 13 15:20:54 2021 +0900
@@ -43,13 +43,12 @@
   factm = {!!}
   fact : (n : ℕ ) → n < (suc (factorial (suc m))) →   gcd (suc (factorial (suc m))) n ≡ 1
   fact n lt = begin
-     gcd (suc (factorial (suc m))) n ≡⟨ {!!}  ⟩
-     -- ? ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor d ) ⟩
-     gcd ( (Dividable.factor d * n + 0) + 1)  n   ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (Dividable.factor d * n) 0) ⟩
-     gcd ( Dividable.factor d * n + 1)  n   ≡⟨  gcdmul+1 (Dividable.factor d)  n  ⟩
+     gcd (suc (factorial (suc m))) n ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor {!!}) ⟩
+     gcd ( (NonPrime.factor d * n + 0) + 1)  n   ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (NonPrime.factor d * n) 0) ⟩
+     gcd ( NonPrime.factor d * n + 1)  n   ≡⟨  gcdmul+1 (NonPrime.factor d)  n  ⟩
      1 ∎  where
-       d :  Dividable n (factorial (suc m ))
+       d :  NonPrime (factorial (suc m ))
        d with <-cmp n (suc m)
-       ... | tri< a ¬b ¬c = factm n (suc m) {!!}
-       ... | tri≈ ¬a b ¬c = factm n (suc m) {!!}
-       ... | tri> ¬a ¬b c = NonPrime.dividable (nonPrime ? ? )
+       ... | tri< a ¬b ¬c = record { factor = {!!} ; dividable = factm n (suc m) {!!} } 
+       ... | tri≈ ¬a b ¬c = record { factor = {!!} ; dividable = factm n (suc m) {!!} } 
+       ... | tri> ¬a ¬b c = nonPrime {!!} {!!}