law bad_none

lawful-fields@0.1.1.0 · proof_num.bend:315

import Base
import lawful-fields@0.1.1.0/defs.bend as F

315law bad_none:
316  for +m: Maybe<&2, Nat>
317  for +M: Nat
318  for +hb: Bad(m, M)
319  {F.decb.of(m, M) == None{} : Maybe<&2, Nat>}