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;