(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/didactic/deriv".
+
include "reals.ma".
interpretation "function power" 'elev x y =
(cic:/matita/didactic/deriv/felev.con x y).
+
+axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).