(* *)
(**************************************************************************)
-include "nat/nat.ma".
+include "nat/big_ops.ma".
include "algebra/unital_magmas.ma".
include "algebra/abelian_magmas.ma".
| napply O
| #x; napply refl
| #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
-nqed.
\ No newline at end of file
+nqed.
+
+ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.
\ No newline at end of file