+check 1 + 2 + 3.
+check 1 + (2 + 3).
+
+notation "a + b" left associative for @{ 'plus $a $b }.
+notation "a * b" left associative for @{ 'mult $a $b }.
+interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
+render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.