affeldt-aist

I think that in other situations similar needs to work with `1 - q` and `1- q ^ n` expressions will occur (we have been using such expressions a lot...

> 1. Is `onemN` necessary? It seems to break the abstraction by producing an actually negative number. I also see you end up using it in the proofs. As far...

We should maybe merge this one. @strub Do you want to squash some of the last commits which do not look informative? ("merge remote-tracking...", commit without commit message, "merge branch...

> We should maybe merge this one. Sorry, I didn't realize it was not yet completed. Or are the Admitted's irrelevant?

Any progress?

I tried to simplify a bit the scripts. Tell me if I introduced to much mess, Maybe it is worth doing one more pass and discuss whether to put lemmas...

> As `bounded_landau` depends of the newly introduced defininition `bounded_fun_norm`, > shouldn't it stay in near Banach-Steinhaus theorem for the time being ? I was thinking that `bounded_fun_norm` would go...

Follow-up to Friday's meeting: I tried to replace `floor_nat_comp` with more primitive lemmas and the usage of `ceil`.

NB: This PR uses the lemma `gtz0_norm` expecting it to be integrated into MathComp. This is rather this lemma: ``` Lemma natr_absz i : `|i|%:R = `|i|%:~R :> R. Proof....

This is being taken care of by https://github.com/math-comp/math-comp/pull/859 .