def clipped_end

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:99

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

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