+ | Add a b => evalA a s\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6evalA b s
+ | Sub a b => evalA a s\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6evalA b s
+ | Mul a b => evalA a s\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6evalA b s
+ | Div a b => \ 5a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"\ 6div\ 5/a\ 6 (evalA a s) (evalA b s)
+ | Mod a b => \ 5a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"\ 6mod\ 5/a\ 6 (evalA a s) (evalA b s)
+ ]