1	# Shared natural-number addition laws; induction is on a symbolic operand.
2	import Base
3	
4	law successor_right:
5	  for +a: Nat
6	  for +b: Nat
7	  {Nat.add(a,1n+b) == 1n+Nat.add(a,b) : Nat}
8	
9	def successor_right(a,b):
10	  match a:
11	    case 0n:
12	      {==}
13	    case 1n+ +p:
14	      %successor_right(p,b) : {1n+Nat.add(p,1n+b) == 1n+_ : Nat}
15	      {==}
16	
17	law double:
18	  for +n: Nat
19	  {Nat.add(n,n) == Nat.double(n) : Nat}
20	
21	def double(n):
22	  match n:
23	    case 0n:
24	      {==}
25	    case 1n+ +p:
26	      %double(p) : {1n+Nat.add(p,1n+p) == 2n+_ : Nat}
27	      %successor_right(p,p) : {1n+Nat.add(p,1n+p) == 1n+_ : Nat}
28	      {==}
29	
30	law zero_right:
31	  for +n: Nat
32	  {Nat.add(n,0n) == n : Nat}
33	
34	def zero_right(n):
35	  match n:
36	    case 0n:
37	      {==}
38	    case 1n+ +p:
39	      %zero_right(p) : {1n+Nat.add(p,0n) == 1n+_ : Nat}
40	      {==}
41	
42	law successor_width:
43	  for +width: Nat
44	  {Nat.add(width,1n) == 1n+width : Nat}
45	
46	def successor_width(width):
47	  match width:
48	    case 0n:
49	      {==}
50	    case 1n+ +rest:
51	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(rest,1n),1n+rest,successor_width(rest))
52	
53	law associative:
54	  for +first: Nat
55	  for +second: Nat
56	  for +third: Nat
57	  {Nat.add(Nat.add(first,second),third) == Nat.add(first,Nat.add(second,third)) : Nat}
58	
59	def associative(first,second,third):
60	  match first:
61	    case 0n:
62	      {==}
63	    case 1n+ +rest:
64	      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(Nat.add(rest,second),third),Nat.add(rest,Nat.add(second,third)),associative(rest,second,third))
65