def earlier_split

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:278

import Base

278def earlier_split(+a: Nat, +b: Nat, earlier: {Nat.is_lt(a, 1n+b) == True{} : Bool}) ->
279  Either<&2, &2, {Nat.is_lt(a, b) == True{} : Bool}, {a == b : Nat}>:
280  match a b:
281    case 0n 0n:
282      Inr{{==}}
283    case 0n 1n+q:
284      Inl{{==}}
285    case 1n+p 0n:
286      Empty.absurd(Either<&2, &2, {Nat.is_lt(1n+p, 0n) == True{} : Bool}, {1n+p == 0n : Nat}>, no_earlier_zero(p, earlier))
287    case 1n+p 1n+q:
288      earlier_lift(p, q, earlier_split(p, q, earlier))