(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/didactic/ex_deriv".
+
include "deriv.ma".
done.
qed.
-axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).
-
alias symbol "plus" = "natural plus".
alias num (instance 0) = "natural number".
theorem de_prodotto_funzioni: