per cases ( b = 0 or b <> 0 ) ;

suppose b = 0 ; :: thesis: ((a + b) !) mod b is zero

hence ((a + b) !) mod b is zero ; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: ((a + b) !) mod b is zero

then reconsider b = b as non zero Nat ;
b divides (a + b) ! by NEWTON:40;
hence ((a + b) !) mod b is zero by PEPIN:6; :: thesis: verum

end;

end;