assym

Stream: new members

[Yakov Pechersky]

This works:

example (m n : ℕ) (h : m < n) : ¬ n < m := asymm h

But trying to do
rw dif_neg (assym h) as a tactic step says unknown identifier 'assym'. In the same file.

[Bryan Gin-ge Chen]

Do you mean asymm or assym?