def pos_pos

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

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

205def pos_pos(+a: Nat, +b: Nat, +ha: {Nat.is_lt(0n, a) == True{} : Bool}, +hb: {Nat.is_lt(0n, b) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.mul(a, b)) == True{} : Bool}:
206  match a:
207    case 0n:
208      Empty.absurd({Nat.is_lt(0n, Nat.mul(0n, b)) == True{} : Bool}, L.false_true(ha))
209    case 1n+ +ap:
210      pos_mul(ap, b, hb)