\ /
V_______________________________________________________________ *)
+(* To be ported
include "arithmetics/bigops.ma".
definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
|assumption
]
]
-qed. *)
\ No newline at end of file
+qed. *)*)
\ No newline at end of file