--- a/automaton-in-agda/src/root2.agda	Sun Sep 24 13:20:31 2023 +0900
+++ b/automaton-in-agda/src/root2.agda	Sun Sep 24 18:02:04 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module root2 where
 
 open import Data.Nat 
@@ -86,7 +88,7 @@
     df = Dividable.factor dm
     dn : Dividable p n
     dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
-        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin 
+        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ (suc p0) ( begin 
           (df * df * p + 0) * p ≡⟨  cong (λ k → k * p)  (+-comm (df * df * p) 0)  ⟩
           ((df * df) * p  ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
             (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p)  ⟩
@@ -196,7 +198,7 @@
       Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
 
 *<-2 : {x y z : ℕ} → z > 0  → x < y → z * x < z * y   
-*<-2 {x} {y} {suc z} (s≤s z>0) x<y = *-monoʳ-< z x<y
+*<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y
 
 r15 : {p : ℕ} → p > 1 → p < p * p
 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )