#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
qed.
#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
qed.