gistfile1.txt

inductive tup_order : (ℕ × ℕ) → (ℕ × ℕ) → Prop
| base_snd : ∀ a b, tup_order (a, b) (a, nat.succ b)
| base_fst : ∀ a b c, tup_order (a, b) (nat.succ a, c)
| succ_fst : ∀ a b c d e, tup_order (a, b) (c, d) → tup_order (a, b) (nat.succ c, e)
| succ_snd : ∀ a b c d, tup_order (a, b) (c, d) → tup_order (a, b) (c, nat.succ d)

section tuporder 
open tup_order

def tup_order_trans : ∀ {a b c : ℕ × ℕ},
   tup_order a b → tup_order b c
       → tup_order a c
| (_,_) (_,_) (_,_) ord1 (base_snd a b) := succ_snd _ _ _ _ ord1
| (_,_) (_,_) (_,_) ord1 (base_fst h i j) := succ_fst _ _ _ _ _ ord1
| (_,_) (_,_) (_,_) ord1 (succ_fst a b c d e t1) := succ_fst _ _ _ _ _ (tup_order_trans ord1 t1)
| (_,_) (_,_) (_,_) ord1 (succ_snd a b c d t) := succ_snd _ _ _ _ (tup_order_trans ord1 t)