--- a/src/nat.agda	Mon Jun 19 17:57:43 2023 +0900
+++ b/src/nat.agda	Tue Jun 20 12:14:12 2023 +0900
@@ -71,6 +71,17 @@
 y≤max (suc x) zero = z≤n
 y≤max (suc x) (suc y) = s≤s( y≤max x y )
 
+x≤y→max=y : (x y : ℕ) → x ≤ y → max x y ≡ y
+x≤y→max=y zero zero x≤y = refl
+x≤y→max=y zero (suc y) x≤y = refl
+x≤y→max=y (suc x) (suc y) (s≤s x≤y) = cong suc (x≤y→max=y x y x≤y )
+
+y≤x→max=x : (x y : ℕ) → y ≤ x → max x y ≡ x
+y≤x→max=x zero zero y≤x = refl
+y≤x→max=x zero (suc y) ()
+y≤x→max=x (suc x) zero lt = refl
+y≤x→max=x (suc x) (suc y) (s≤s y≤x) = cong suc (y≤x→max=x x y y≤x )
+
 -- _*_ : ℕ → ℕ → ℕ
 -- _*_ zero _ = zero
 -- _*_ (suc n) m = m + ( n * m )