let s, t be Nat; :: thesis: ( s >= t implies for r being Nat st r = s - t holds
s choose t = s choose r )
assume A1: s >= t ; :: thesis: for r being Nat st r = s - t holds
s choose t = s choose r
let r be Nat; :: thesis: ( r = s - t implies s choose t = s choose r )
assume A2: r = s - t ; :: thesis: s choose t = s choose r
A3: s >= r

proof

t - s >= 0 - s by XREAL_1:11;
then - (- s) >= - (t - s) by XREAL_1:26;
hence s >= r by A2; :: thesis: verum

end;

t = s - r by A2;
then s choose r = (s ! ) / ((r ! ) * (t ! )) by A3, Def3;
hence s choose t = s choose r by A1, A2, Def3; :: thesis: verum