NatExtrema.clipped_end: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_extrema.bend as NatExtrema
Lines 99-104 of stelliferous@0.0.2.0/proofs/nat_extrema.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_extrema.bend&start_line=99&end_line=104

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

def clipped_end(+first: Nat,+end: Nat) -> {Nat.add(first,Nat.sub(end,first)) == Nat.max(first,end) : Nat}:
  match first end:
    case 0n +end: Order.subtract_zero(end)
    case 1n+ +first 0n: Order.commutative(1n+first,0n)
    case 1n+ +first 1n+ +end:
      Equal.cong(Nat,Nat,value => 1n+value,Nat.add(first,Nat.sub(end,first)),Nat.max(first,end),clipped_end(first,end))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.max
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=commutative
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=subtract_zero