α : Type ?u.968134
a b : PosNum
this : Ordering.casesOn (PosNum.cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn (cmp (pos a) (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
α : Type ?u.968134
a b : PosNum
⊢ Ordering.casesOn (cmp (pos a) (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
have := PosNum.cmp_to_nat a b
α : Type ?u.968134
a b : PosNum
⊢ Ordering.casesOn (PosNum.cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn (cmp (pos a) (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
α : Type ?u.968134
a b : PosNum
this : Ordering.casesOn (PosNum.cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn (cmp (pos a) (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
revert this
α : Type ?u.968134
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (PosNum.cmp a b) →
    Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (PosNum.cmp a b)
α : Type ?u.968134
a b : PosNum
⊢ Ordering.casesOn (PosNum.cmp a b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn (cmp (pos a) (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))
dsimp [cmp]
no goals
α : Type ?u.968134
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (PosNum.cmp a b) →
    Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (PosNum.cmp a b)
cases PosNum.cmp a b <;> dsimp <;> [simp; exact congr_arg pos; simp [GT.gt]]
α : Type ?u.968134
a b : PosNum
this : Ordering.casesOn (PosNum.cmp b a) (↑b < ↑a) (b = a) (↑a < ↑b)
⊢ Ordering.casesOn (cmp (neg a) (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
α : Type ?u.968134
a b : PosNum
⊢ Ordering.casesOn (cmp (neg a) (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
have := PosNum.cmp_to_nat b a
α : Type ?u.968134
a b : PosNum
⊢ Ordering.casesOn (PosNum.cmp b a) (↑b < ↑a) (b = a) (↑a < ↑b) →
    Ordering.casesOn (cmp (neg a) (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
α : Type ?u.968134
a b : PosNum
this : Ordering.casesOn (PosNum.cmp b a) (↑b < ↑a) (b = a) (↑a < ↑b)
⊢ Ordering.casesOn (cmp (neg a) (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
revert this
α : Type ?u.968134
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) (PosNum.cmp b a) →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) (PosNum.cmp b a)
α : Type ?u.968134
a b : PosNum
⊢ Ordering.casesOn (PosNum.cmp b a) (↑b < ↑a) (b = a) (↑a < ↑b) →
    Ordering.casesOn (cmp (neg a) (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))
dsimp [cmp]
no goals
α : Type ?u.968134
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) (PosNum.cmp b a) →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) (PosNum.cmp b a)
cases PosNum.cmp b a <;> dsimp <;> [simp; simp (config := { contextual := true }); simp [GT.gt]]