α : Type ?u.226784
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.226784
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.226784
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.226784
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.226784
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.226784
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]
case lt
α : Type ?u.226784
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.lt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.lt

case eq
α : Type ?u.226784
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.eq → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.eq

case gt
α : Type ?u.226784
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.gt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.gt
α : Type ?u.226784
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
no goals
case lt
α : Type ?u.226784
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.lt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.lt

case eq
α : Type ?u.226784
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.eq → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.eq

case gt
α : Type ?u.226784
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) Ordering.gt → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) Ordering.gt
exacts [id, congr_arg pos, id]