div.agda

open import Agda.Builtin.Equality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality.Core using (sym; trans; _≢_)
-- open import Data.Nat.Base
open import Data.Nat.Base
  using (ℕ; zero; suc; _+_; _*_; s≤s; z≤n; _≤_; _<_; _>_;
        Ordering; less; equal; greater; compare)
open import Data.Nat.Properties using (+-identityʳ; +-assoc; ≤-trans; m≤m+n; m≢1+m+n; *-cancelˡ-≡)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)

infixr 2 _⋀_

_⋀_ : Set -> Set -> Set
_⋀_ = _×_

infixr 1 _⋁_

_⋁_ : Set -> Set -> Set
_⋁_ = _⊎_

-----

compareX : ∀ m n → Ordering m n
compareX zero    zero    = equal   zero
compareX (suc m) zero    = greater zero m
compareX zero    (suc n) = less    zero n
compareX (suc m) (suc n) with compareX m n
... | less    m k = less (suc m) k
... | equal   m   = equal (suc m)
... | greater n k = greater (suc n) k

lt|eq|gt : ∀ {n m} -> Ordering n m -> n < m ⋁ n ≡ m ⋁ n > m
lt|eq|gt {n} {.(suc (n + k))} (less .n k)     = inj₁ (s≤s (m≤m+n n k))
lt|eq|gt {n} {.n} (equal .n)                  = inj₂ (inj₁ refl)
lt|eq|gt {.(suc (m + k))} {m} (greater .m k)  = inj₂ (inj₂ (s≤s (m≤m+n m k)))

-----

data QuotRem : ℕ -> ℕ -> ℕ -> ℕ -> Set where
  quotRem : ∀ {n m q r} -> n ≡ r + m * q -> 0 ≤ r -> r < m -> QuotRem n m q r

Divisor : ℕ -> ℕ -> ℕ -> Set
Divisor n m q = QuotRem n m q 0

ex1 : QuotRem 5 3 1 2
ex1 = quotRem refl z≤n (s≤s (s≤s (s≤s z≤n)))

ex2 : Divisor 6 3 2
ex2 = quotRem refl z≤n (s≤s z≤n)

toContra : ∀ {ℓ} -> ∀ {A B : Set ℓ} -> (A -> B) -> ¬ B -> ¬ A
toContra f nb a = nb (f a)

contraLemma1 : ∀ n m o -> 1 ≤ n -> n * m ≢ n * suc (m + o)
contraLemma1 (suc n) m o le = toContra (*-cancelˡ-≡ n) (m≢1+m+n m)

uniqueDivisor : ∀ {m q₁ q₂ n : ℕ} -> Divisor n m q₁ -> Divisor n m q₂ -> q₁ ≡ q₂
uniqueDivisor {m} {q₁} {q₂} (quotRem eq₁ _ mp₁) (quotRem eq₂ _ mp₂)
              with compare q₁ q₂
...              | equal .q₁        = refl
uniqueDivisor {m} {q₁} {q₂} (quotRem eq₁ _ mp₁) (quotRem eq₂ _ mp₂)
                 | less .q₁ k    with contraLemma1 m q₁ k mp₁ (trans (sym eq₁) eq₂)
...                                 | ()
uniqueDivisor {m} {q₁} {q₂} (quotRem eq₁ _ mp₁) (quotRem eq₂ _ mp₂)
                 | greater .q₂ k with contraLemma1 m q₂ k mp₂ (trans (sym eq₂) eq₁)
...                                 | ()


uniqueQuotRem : ∀ {m q₁ q₂ r₁ r₂ n : ℕ} -> QuotRem n m q₁ r₁ -> QuotRem n m q₂ r₂ -> q₁ ≡ q₂ ⋀ r₁ ≡ r₂
uniqueQuotRem {m} {q₁} {q₂} (quotRem eq₁ _ rm₁) (quotRem eq₂ _ rm₂)
              with compare q₁ q₂
...  | less .q₁ k = {!!}
...  | equal .q₁ = refl , {!!}
...  | greater .q₂ k = {!!}

div.v

(* Require Import Logic. *)
Require Import Arith.

Inductive Ordering : nat -> nat -> Type :=
| less     : forall m k, Ordering m (S (m + k))
| equal    : forall m,   Ordering m m
| greater  : forall m k, Ordering (S (m + k)) m
.

Fixpoint compare (m n : nat) : Ordering m n :=
  match n with
  | O    =>  match m with
             | O    => equal O
             | S m1 => greater O m1
             end
  | S n1 =>  match m with
             | O    => less O n1
             | S m1 => match (compare m1 n1) with
                       | less m2 k     => less (S m2) k
                       | equal m2      => equal (S m2)
                       | greater n2 k  => greater (S n2) k
                       end
             end
  end
.

Print le.

(*
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.
 *)

Lemma lt_eq_gt : forall n m, Ordering n m -> n < m \/ n = m \/ n > m.
  intros n m OH.
  inversion OH.
  - left.
    rewrite <- (plus_Sn_m n k).
    exact (le_plus_l (S n) k).
  - right. left.
    reflexivity.
  - right. right.
    rewrite <- (plus_Sn_m m k).
    exact (le_plus_l (S m) k).
Defined.