law is_eq_comm

bend-mathlib@0.8.1.0 · nat.bend:1278

import Base

1278# The equality test is symmetric.
1279law is_eq_comm:
1280  for a: Nat
1281  for b: Nat
1282  {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}