Have notations for deriving and derivability

[CohenCyril]

Provide and document derivation notations such as:

• f^`(n), f^`() and f^`N(n) (as in poly.v) for derivation onR (and when available, on C)
• 'D(A -> V) for the type of derviable functions from domain A to a normed module type V
• 'D^n(A -> V) for n times derivable (so that 'D^1 = 'D)
• 'C^n_(A -> V) (I believe 'C^0 = 'C in the literature, but I advocate for not providing a notation without explicit n)

Bonus question: should the last 3 be types or sets ?

[affeldt-aist]

f^(n), f^() and f^`N(n) (as in poly.v) for derivation onR (and when available, on C)

I gave a try to f^() and f^(n) in a branch issue68. I experimented with 'D_v[f] for the directional derivative also:

analysis/derive.v

Lines 33 to 40 in a38af7f

	Reserved Notation "'J_ p [ f ]" (at level 10,
	p, f at next level, format "''J_' p [ f ]").
	Reserved Notation "'D_ v [ f ]" (at level 10,
	v, f at next level, format "''D_' v [ f ]").
	Reserved Notation "'D '_' v [ f ] c" (at level 10,
	v, f at next level, format "''D' '_' v [ f ] c"). (* printing *)
	Reserved Notation "f ^` ()" (at level 8, format "f ^` ()").
	Reserved Notation "f ^` ( n )" (at level 8, format "f ^` ( n )").

Bonus question: should the last 3 be types or sets ?

Mmmhhh. The proposed notation looks more appropriate for a type but it seems to me that the current formalization lends itself more easily to sets.