def is_eq_sym_false

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:555

import Base

555def is_eq_sym_false(+a: Nat, +b: Nat, +h: {Nat.is_eq(a, b) == False{} : Bool}) -> {Nat.is_eq(b, a) == False{} : Bool}:
556  match a b:
557    case 0n 0n:
558      h
559    case 0n 1n+q:
560      {==}
561    case 1n+p 0n:
562      {==}
563    case 1n+p 1n+q:
564      is_eq_sym_false(p, q, h)