module Two where

open import Logic
open import Equality

-- Definition (The set ₂ of binary numbers).

data  : Set where
  : 
  : 


two-equality-cases : {A : Ω}  
-------------------------------------------
 ∀{b : }  (b    A)  (b    A)  A
-------------------------------------------
two-equality-cases {A} {} f₀ f₁ = f₀ refl
two-equality-cases {A} {} f₀ f₁ = f₁ refl


Lemma[b≡₁→b≠₀] :  
--------------------------
  ∀{b : }  b    b  
--------------------------
Lemma[b≡₁→b≠₀] {} () 
Lemma[b≡₁→b≠₀] {} r = λ ()


Lemma[b≠₀→b≡₁] :  
--------------------------
  ∀{b : }  b    b  
--------------------------
Lemma[b≠₀→b≡₁] {} f = ⊥-elim(f refl)
Lemma[b≠₀→b≡₁] {} f = refl


Lemma[b≠₁→b≡₀] :  
--------------------------
  ∀{b : }  b    b  
--------------------------
Lemma[b≠₁→b≡₀] {} f = refl
Lemma[b≠₁→b≡₀] {} f = ⊥-elim(f refl)


Lemma[b≡₀→b≠₁] :  
--------------------------
  ∀{b : }  b    b  
--------------------------
Lemma[b≡₀→b≠₁] {} r = λ ()
Lemma[b≡₀→b≠₁] {} () 


Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] : 
----------------------------------------------
  ∀{a b : }  (a    b  )  b    a  
----------------------------------------------
Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] f = 
  Lemma[b≠₁→b≡₀]  (contra-positive f)  Lemma[b≡₀→b≠₁]


Lemma[[a≡₀→b≡₀]→b≡₁→a≡₁] : 
----------------------------------------------
  ∀{a b : }  (a    b  )  b    a  
----------------------------------------------
Lemma[[a≡₀→b≡₀]→b≡₁→a≡₁] f = 
  Lemma[b≠₀→b≡₁]  (contra-positive f)  Lemma[b≡₁→b≠₀]


-- Definition (Natural order of binary numbers)
_≤_ : (a b : )  Ω
a  b = a    b  

_≥_ : (a b : )  Ω
a  b = b  a


-- Definition (Minimum of binary numbers).
min :     
min  b = 
min  b = b


Lemma[minab≤a] : 
----------------------------
  ∀{a b : }  min a b   a
----------------------------
Lemma[minab≤a] {} {b} r = ⊥-elim(Lemma[b≡₁→b≠₀] r refl)
Lemma[minab≤a] {} {b} r = refl