--- a/automaton-in-agda/src/root2.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/root2.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -197,8 +197,24 @@
       d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
       Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
 
+-- data _≤_ : (i j : ℕ) → Set where
+--    z≤n : {n : ℕ} → zero ≤ n
+--    s≤s : {i j : ℕ} → i ≤ j → (suc i) ≤ (suc j)
+
 *<-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 {zero} {suc y} {suc z} (s≤s z>0) x<y = begin
+   suc (z * zero) ≡⟨ cong suc (*-comm z _) ⟩ 
+   suc (zero * z) ≡⟨ refl ⟩ 
+   suc zero ≤⟨ s≤s z≤n ⟩ 
+   suc (y + z * suc y) ∎ where open ≤-Reasoning
+*<-2 {x} {y} {suc zero} (s≤s z>0) x<y = begin
+   suc (x + zero) ≡⟨ cong suc (+-comm x _) ⟩
+   suc x  ≤⟨ x<y ⟩
+   y  ≡⟨ +-comm zero _ ⟩
+   y + zero  ∎ where open ≤-Reasoning
+*<-2 {x} {y} {suc (suc z)} (s≤s z>0) x<y = begin
+   suc (x + (x + z * x))  <⟨ +-mono-≤-< x<y (*<-2 {x} {y} {suc z} (s≤s z≤n) x<y) ⟩
+   y + (y + z * y)  ∎ where open ≤-Reasoning
 
 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 )