n + 1 > 0 + 1 by XREAL_1:6;
then A1: n >= 1 by NAT_1:13;

per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;

suppose n = 1 ; :: thesis: ( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative )

hence ( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative ) by INT_3:10; :: thesis: verum

end;

suppose n > 1 ; :: thesis: ( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative )

hence ( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative ) by INT_3:11; :: thesis: verum

end;

end;