def equal_symmetric

stelliferous@0.0.2.0 · proofs/nat_order.bend:119

import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder

import Base

119def equal_symmetric(+left: Nat,+right: Nat) -> {Nat.is_eq(left,right) == Nat.is_eq(right,left) : Bool}:
120  match left right:
121    case 0n 0n: {==}
122    case 0n 1n+right: {==}
123    case 1n+left 0n: {==}
124    case 1n+left 1n+right: equal_symmetric(left,right)

Uses (3)

Used by (2)