law is_eq_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:4247

import Base

4247# The equality test is symmetric, reversed to rewrite toward the simple side.
4248law is_eq_comm_sym:
4249  for a: Nat
4250  for b: Nat
4251  {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}