interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
render cic:/Coq/Arith/Plus/plus_comm.con.
-notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
-notation \[ \TERM a * \TERM b \] for 'mult \TERM a \TERM b.
+notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
+notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM 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.