Axiom addeq | index | src |

Addition respects equalty.

axiom addeq (a b c d: nat): $ a = b -> c = d -> a + c = b + d $;