α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn (cmp (bit0 a) (bit0 b)) (↑(bit0 a) < ↑(bit0 b)) (bit0 a = bit0 b) (↑(bit0 b) < ↑(bit0 a))
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp (bit0 a) (bit0 b)) (↑(bit0 a) < ↑(bit0 b)) (bit0 a = bit0 b) (↑(bit0 b) < ↑(bit0 a))
have := cmp_to_nat a b
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn (cmp (bit0 a) (bit0 b)) (↑(bit0 a) < ↑(bit0 b)) (bit0 a = bit0 b) (↑(bit0 b) < ↑(bit0 a))
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn (cmp (bit0 a) (bit0 b)) (↑(bit0 a) < ↑(bit0 b)) (bit0 a = bit0 b) (↑(bit0 b) < ↑(bit0 a))
revert this
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit0 ↑a < _root_.bit0 ↑b

case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ bit0 a = bit0 b

case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit0 ↑b < _root_.bit0 ↑a
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn (cmp (bit0 a) (bit0 b)) (↑(bit0 a) < ↑(bit0 b)) (bit0 a = bit0 b) (↑(bit0 b) < ↑(bit0 a))
cases cmp a b <;> dsimp <;> intro this
no goals
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit0 ↑a < _root_.bit0 ↑b
exact add_lt_add this this
no goals
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ bit0 a = bit0 b
rw [this]
no goals
case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit0 ↑b < _root_.bit0 ↑a
exact add_lt_add this this
α : Type ?u.145219
a b : PosNum
⊢ Ordering.rec (_root_.bit0 ↑a < _root_.bit1 ↑b) (bit0 a = bit1 b) (_root_.bit1 ↑b < _root_.bit0 ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (cmp a b))
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp (bit0 a) (bit1 b)) (↑(bit0 a) < ↑(bit1 b)) (bit0 a = bit1 b) (↑(bit1 b) < ↑(bit0 a))
dsimp [cmp]
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (_root_.bit0 ↑a < _root_.bit1 ↑b) (bit0 a = bit1 b) (_root_.bit1 ↑b < _root_.bit0 ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (cmp a b))
α : Type ?u.145219
a b : PosNum
⊢ Ordering.rec (_root_.bit0 ↑a < _root_.bit1 ↑b) (bit0 a = bit1 b) (_root_.bit1 ↑b < _root_.bit0 ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (cmp a b))
have := cmp_to_nat a b
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (_root_.bit0 ↑a < _root_.bit1 ↑b) (bit0 a = bit1 b) (_root_.bit1 ↑b < _root_.bit0 ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (cmp a b))
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (_root_.bit0 ↑a < _root_.bit1 ↑b) (bit0 a = bit1 b) (_root_.bit1 ↑b < _root_.bit0 ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (cmp a b))
revert this
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit0 ↑a < _root_.bit1 ↑b

case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑a < _root_.bit1 ↑b

case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit1 ↑b < _root_.bit0 ↑a
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (_root_.bit0 ↑a < _root_.bit1 ↑b) (bit0 a = bit1 b) (_root_.bit1 ↑b < _root_.bit0 ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (cmp a b))
cases cmp a b <;> dsimp <;> intro this
no goals
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit0 ↑a < _root_.bit1 ↑b
exact Nat.le_succ_of_le (add_lt_add this this)
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑b < _root_.bit1 ↑b
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑a < _root_.bit1 ↑b
rw [this]
no goals
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑b < _root_.bit1 ↑b
apply Nat.lt_succ_self
no goals
case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit1 ↑b < _root_.bit0 ↑a
exact cmp_to_nat_lemma this
α : Type ?u.145219
a b : PosNum
⊢ Ordering.rec (_root_.bit1 ↑a < _root_.bit0 ↑b) (bit1 a = bit0 b) (_root_.bit0 ↑b < _root_.bit1 ↑a)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (cmp a b))
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp (bit1 a) (bit0 b)) (↑(bit1 a) < ↑(bit0 b)) (bit1 a = bit0 b) (↑(bit0 b) < ↑(bit1 a))
dsimp [cmp]
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (_root_.bit1 ↑a < _root_.bit0 ↑b) (bit1 a = bit0 b) (_root_.bit0 ↑b < _root_.bit1 ↑a)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (cmp a b))
α : Type ?u.145219
a b : PosNum
⊢ Ordering.rec (_root_.bit1 ↑a < _root_.bit0 ↑b) (bit1 a = bit0 b) (_root_.bit0 ↑b < _root_.bit1 ↑a)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (cmp a b))
have := cmp_to_nat a b
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (_root_.bit1 ↑a < _root_.bit0 ↑b) (bit1 a = bit0 b) (_root_.bit0 ↑b < _root_.bit1 ↑a)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (cmp a b))
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (_root_.bit1 ↑a < _root_.bit0 ↑b) (bit1 a = bit0 b) (_root_.bit0 ↑b < _root_.bit1 ↑a)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (cmp a b))
revert this
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit1 ↑a < _root_.bit0 ↑b

case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑b < _root_.bit1 ↑a

case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit0 ↑b < _root_.bit1 ↑a
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (_root_.bit1 ↑a < _root_.bit0 ↑b) (bit1 a = bit0 b) (_root_.bit0 ↑b < _root_.bit1 ↑a)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (cmp a b))
cases cmp a b <;> dsimp <;> intro this
no goals
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit1 ↑a < _root_.bit0 ↑b
exact cmp_to_nat_lemma this
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑b < _root_.bit1 ↑b
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑b < _root_.bit1 ↑a
rw [this]
no goals
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ _root_.bit0 ↑b < _root_.bit1 ↑b
apply Nat.lt_succ_self
no goals
case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit0 ↑b < _root_.bit1 ↑a
exact Nat.le_succ_of_le (add_lt_add this this)
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn (cmp (bit1 a) (bit1 b)) (↑(bit1 a) < ↑(bit1 b)) (bit1 a = bit1 b) (↑(bit1 b) < ↑(bit1 a))
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp (bit1 a) (bit1 b)) (↑(bit1 a) < ↑(bit1 b)) (bit1 a = bit1 b) (↑(bit1 b) < ↑(bit1 a))
have := cmp_to_nat a b
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn (cmp (bit1 a) (bit1 b)) (↑(bit1 a) < ↑(bit1 b)) (bit1 a = bit1 b) (↑(bit1 b) < ↑(bit1 a))
α : Type ?u.145219
a b : PosNum
this : Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn (cmp (bit1 a) (bit1 b)) (↑(bit1 a) < ↑(bit1 b)) (bit1 a = bit1 b) (↑(bit1 b) < ↑(bit1 a))
revert this
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit1 ↑a < _root_.bit1 ↑b

case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ bit1 a = bit1 b

case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit1 ↑b < _root_.bit1 ↑a
α : Type ?u.145219
a b : PosNum
⊢ Ordering.casesOn (cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn (cmp (bit1 a) (bit1 b)) (↑(bit1 a) < ↑(bit1 b)) (bit1 a = bit1 b) (↑(bit1 b) < ↑(bit1 a))
cases cmp a b <;> dsimp <;> intro this
no goals
case lt
α : Type ?u.145219
a b : PosNum
this : ↑a < ↑b
⊢ _root_.bit1 ↑a < _root_.bit1 ↑b
exact Nat.succ_lt_succ (add_lt_add this this)
no goals
case eq
α : Type ?u.145219
a b : PosNum
this : a = b
⊢ bit1 a = bit1 b
rw [this]
no goals
case gt
α : Type ?u.145219
a b : PosNum
this : ↑b < ↑a
⊢ _root_.bit1 ↑b < _root_.bit1 ↑a
exact Nat.succ_lt_succ (add_lt_add this this)