def pos_mul

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/fact.bend:36

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

36def pos_mul(+p: Nat, +f: Nat, +h: {Nat.is_lt(0n, f) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.mul(1n+p, f)) == True{} : Bool}:
37  match f:
38    case 0n:
39      Empty.absurd({Nat.is_lt(0n, Nat.mul(1n+p, 0n)) == True{} : Bool}, L.false_true(h))
40    case 1n+fp:
41      {==}