Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment