E:(
Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y)) 
(
h:(). (n,k:. (n E k) 
h(n) = h(k)) & (n:. n E (h(n))))
comp_choice
== {i:
| 0
i }
Thm* E:(Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y))
(h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n))))
comp_choice
Thm* E:(
), n,k:.
(EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk })
min_el_iff
Thm* E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn })
min_el_sound
Thm* E:(), n,k:.
(EquivRel x,y:. x E y) (n E k) Min{ x | xEn } = Min{ x | xEk }
min_el_unique
Thm* f:(), n,k:.
f(n) = f(k) MinArg(f : {0..n
}) = MinArg(f : {0..k}) 
min_arg_iff
Thm* f:(), n:. f(MinArg(f : {0..n})) = f(n) min_arg_sound
Thm* f:(), n,k:.
f(n) = f(k) MinArg(f : {0..n}) = MinArg(f : {0..k})
min_arg_unique
Thm* f:(), n:, i:(n+1). f(n-MinAr(f;i;n)) = f(n) min_ar_sound
Thm* f:(), n:, i:(n+1), j:(n-i+1).
f(n-i) = f(n) MinAr(f;j+i;n) = MinAr(f;j;n-i)+i
min_ar_alt
Thm* f:(), n:, i:(n+1). MinAr(f;i;n) (i+1) min_ar_wf