α : Type ?u.981446
m n : ZNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt
α : Type ?u.981446
m n : ZNum
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt
simp at h
no goals
α : Type ?u.981446
m n : ZNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt
simp [h]
α : Type ?u.981446
m n : ZNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt
α : Type ?u.981446
m n : ZNum
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt
simp at h
no goals
α : Type ?u.981446
m n : ZNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt
simp [h, lt_irrefl]
no goals
α : Type ?u.981446
m n : ZNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt
simp [not_lt_of_gt h]