Peano arithmetic as an introduction to prolog

peano.pl

%load a prolog file like [this].
%or just send file to REPL

%Peano arithmetic
% https://en.wikipedia.org/wiki/Peano_axioms
% * 0 is a natural number
% * if n is a natural number, s(n) is a natural number
% * equality
%   * 0 = 0
%   * a = b -> s(a) = s(b)
% * Addition
%  * a + 0 = a
%  * a + s(b) = s(a + b)
% * Multiplication
%  * 0 x a = 0
%  * s(a) x b = (a x b) + b

%Knowledge base
%Facts (||)
%Queries
%Variables
%Rules

is_number(0).
is_number(s(N)) :- is_number(N).

eq(0,0).
eq(s(M),s(N)) :- eq(M,N).

sum(A, 0, A).
sum(A, s(B), s(C)) :-
	sum(A, B, C).

mul(0,_,0).
mul(s(A),B,C) :-
    mul(A,B,D), sum(D,B,C).

Hello! What about this?

eq(sum(A, o), A).
eq(sum(A, s(B)), s(sum(A, B))).

% how to get the proof of 1 + 1 = 2
% eq(sum(s(o), s(o)), I), eq(I, s(s(o))).
% will produce I = s(sum(s(o), o)) .

eq(A, C) :- eq(A, B), eq(B, C).