def minimum_when_ordered

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:31

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

31def minimum_when_ordered(+left: Nat,+right: Nat,ordered: {Nat.is_le(left,right) == True{} : Bool}) -> {Nat.min(left,right) == left : Nat}:
32  match left right:
33    case 0n right: {==}
34    case 1n+left 0n: Empty.absurd({Nat.min(1n+left,0n) == 1n+left : Nat},WordEncoding.false_true(ordered))
35    case 1n+ +left 1n+ +right:
36      Equal.cong(Nat,Nat,n => 1n+n,Nat.min(left,right),left,minimum_when_ordered(left,right,ordered))