# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585370336 -32400
# Node ID 9f5bf86fe6dd266fa242b239f0489e5ac132a008
# Parent  e35d729efd5859c925f5281f723b1be34894a961
fix uniquness

diff -r e35d729efd58 -r 9f5bf86fe6dd nat.agda
--- a/nat.agda	Fri Mar 27 14:37:08 2020 +0900
+++ b/nat.agda	Sat Mar 28 13:38:56 2020 +0900
@@ -8,7 +8,7 @@
 open import  Relation.Binary.PropositionalEquality
 open import  Relation.Binary.Core
 open import  logic
-open import Relation.Binary.Definitions
+-- open import Relation.Binary.Definitions
 
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
diff -r e35d729efd58 -r 9f5bf86fe6dd prob1.agda
--- a/prob1.agda	Fri Mar 27 14:37:08 2020 +0900
+++ b/prob1.agda	Sat Mar 28 13:38:56 2020 +0900
@@ -9,8 +9,15 @@
 open import Data.Empty
 open import Data.Product
 open import Relation.Nullary
+<<<<<<< working copy
+
+||||||| base
+
+
+=======
 open import Relation.Binary.Definitions
 
+>>>>>>> destination
 -- All variables are positive integer
 -- A = -M*n + i +k*M  - M
 -- where n is in range (0,…,k-1) and i is in range(0,…,M-1)