]
].
-coercion cic:/matita/demo/power_derivative/inj.con.
+coercion inj.
axiom Rplus_Rzero_x: ∀x:R.0+x=x.
axiom Rplus_comm: symmetric ? Rplus.
definition costante : nat → R → R ≝
λa:nat.λx:R.inj a.
-coercion cic:/matita/demo/power_derivative/costante.con 1.
+coercion costante with 1.
axiom f_eq_extensional:
∀f,g:R→R.(∀x:R.f x = g x) → f=g.