Discrete and continuous abel transforms

[Tragicus]

Motivation for this change

Abel transforms and a few helper lemmas, as part of #1720.

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

[Tragicus]

I forgot to credit the main author, which is very silly, I will do it with the first round of reviews.

[affeldt-aist]

Suggested change

	Lemma floor_nat (R : archiNumDomainType) n : absz (floor (n%:R : R)) = n.
	Proof.
	apply: (can_inj absz_nat).
	rewrite gez0_abs; first by rewrite real_floor_ge0.
	by apply /(@intr_inj R) /eqP; rewrite -[_ == _]intrEfloor.
	Qed.
	Lemma floor_nat (R : archiNumDomainType) n : floor (n%:R : R) = n.
	Proof. by apply/(@intr_inj R)/eqP; rewrite -[_ == _]intrEfloor. Qed.
	Lemma absz_floor_nat (R : archiNumDomainType) n : `|floor (n%:R : R)|%N = n.
	Proof.
	by apply: (can_inj absz_nat); rewrite gez0_abs ?real_floor_ge0// floor_nat.
	Qed.