is_derive1_sqrt lemma

[yosakaon]

Co-authored with @affeldt-aist

Motivation for this change

This PR introduces the lemma is_derive1_sqrt, establishing the derivability of the square root function at any strictly positive real number and provides its derivative formula.
This result is essential to prove of the derivability of the norm function and such calculations.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

the proof script can be compressed a lot (@affeldt-aist will be good at that)

[t6s]

looks good

[CohenCyril]

I didn't have time to finish the review
Thanks for the contribution. I had a small remark.

[CohenCyril]

This looks redundant with sqr_sqrt, (and slightly weaker since Num.pos can be weakened to Num.nneg).
If kept, it should be generalized and renamed sqrtK (the prefix of a K lemma is the section / thing being cancelled)

[affeldt-aist]

Sorry for having been too hasty, will fix asap in a new PR.

[CohenCyril]

(an in the long run, we should actually replace sqr_sqrt which has an equivalent statement written in an expanded way and which name is not as canonical as sqrtK)