def reflexive

stelliferous@0.0.2.0 · proofs/nat_order.bend:133

import Base

133def reflexive(+a: Nat) -> {Nat.is_le(a,a) == True{} : Bool}:
134  match a:
135    case 0n:
136      {==}
137    case 1n+p:
138      reflexive(p)