use(int_addition).
use(int_induction,[prop=comm_plus]).
use(int_induction,[prop=assoc_plus]).


comm_plus(Y)==all(X,X+Y=Y+X).
assoc_plus(Z)==all(X,all(Y,(X+Y)+Z=X+(Y+Z))).