def earlier_split

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:281

import Base

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