let p be Prime; :: thesis: for n being odd Nat st n < p holds
( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 )
let n be odd Nat; :: thesis: ( n < p implies ( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 ) )
assume A1: n < p ; :: thesis: ( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 )

per cases ( p is even or p is odd ) ;

suppose p is even ; :: thesis: ( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 )

then B1: p = 2 by LAGRA4SQ:13;
then n = 1 by A1, NAT_1:23;
then ( ((p - 1) choose (n - 1)) mod 2 = 1 mod (1 + 1) & ((p - 1) choose n) mod 2 = 1 mod (1 + 1) ) by B1, NEWTON:19;
hence ( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 ) by B1; :: thesis: verum

end;

suppose p is odd ; :: thesis: ( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 )

then reconsider p = p as odd Nat ;
reconsider m = (n - 1) / 2 as Nat ;
(2 * m) + 1 < p by A1;
hence ( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 ) by LmPCZ; :: thesis: verum

end;

end;