Theorem: Nat.compare_gt (Algdata/Init/Nat.lean)

State before:
m n : Nat
⊢ m > n → compare m n = Ordering.gt
Tactic:
intro h
State after:
m n : Nat
h : m > n
⊢ compare m n = Ordering.gt

State before:
m n : Nat
h : m > n
⊢ compare m n = Ordering.gt
Tactic:
simp [compare, instOrdNat, compareOfLessAndEq]
State after:
m n : Nat
h : m > n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.gt

State before:
m n : Nat
h : m > n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.gt
Tactic:
rw [if_neg (Nat.lt_asymm h), if_neg (Nat.ne_of_lt h).symm]
State after:
no goals