let s, t be Nat; :: thesis: ( s >= 1 & t = s - 1 implies s choose t = s )
assume A1: ( s >= 1 & t = s - 1 ) ; :: thesis: s choose t = s
then s choose t = s choose 1 by Th30;
hence s choose t = s by A1, Th33; :: thesis: verum