# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585507830 -32400
# Node ID 805986409de411ea3ac611808cce309e546722d3
# Parent  0b53b08e7ae43efe13369ba42dad1b11a77f88af
u1 done

diff -r 0b53b08e7ae4 -r 805986409de4 nat.agda
--- a/nat.agda	Mon Mar 30 02:10:49 2020 +0900
+++ b/nat.agda	Mon Mar 30 03:50:30 2020 +0900
@@ -129,6 +129,9 @@
 <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
 <-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
 
+<<+ : {x y z w : ℕ } → x < y → w < z  → x + w < y + z 
+<<+ {x} {y} {z} {w} x<y w<z = <-trans ( <-plus {_} {_} {w } x<y ) ( <-plus-0 w<z )
+
 ≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
 ≤-plus {0} {y} {zero} z≤n = z≤n
 ≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y 
@@ -138,6 +141,9 @@
 ≤-plus-0 {x} {y} {zero} lt = lt
 ≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )
 
+<≤+ : {x y z w : ℕ } → x < y → w ≤ z  → x + w < y + z 
+<≤+ {x} {y} {z} {w} x<y w≤z  = ≤-trans ( <-plus {_} {_} {w } x<y ) ( ≤-plus-0 w≤z )
+
 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z 
 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
 x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
diff -r 0b53b08e7ae4 -r 805986409de4 prob1.agda
--- a/prob1.agda	Mon Mar 30 02:10:49 2020 +0900
+++ b/prob1.agda	Mon Mar 30 03:50:30 2020 +0900
@@ -174,7 +174,21 @@
         lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
         lemma5 : {m1  : ℕ} →      M * suc m1 + A  < M * suc n + A
                            → M + (M * suc m1 + A) ≤ M * suc n + A  
-        lemma5 = {!!}
+        lemma5 {m1} lt with <-cmp m1 n
+        lemma5 {m1} lt | tri< a ¬b ¬c = begin
+                   M + (M * suc m1 + A)
+               ≡⟨ sym (+-assoc M _ _ ) ⟩
+                   (M + M * suc m1) + A
+               ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩
+                   (M * suc zero + M * suc m1) + A
+               ≡⟨  sym ( cong (λ k → k + A) (( proj₁ *-distrib-+  )  M (suc zero) _ )) ⟩
+                   M * suc (suc m1) + A
+               ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M )  (*≤ (s≤s a))) ⟩
+                   M * suc n + A
+               ∎ where open ≤-Reasoning
+        lemma5 {m1} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt )
+        lemma5 {m1} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c)
+                (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c)))))))
         lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i
         lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin 
                  M + x + j