proposition: Lemma expf_ge1 : forall m (x : F), x >= 1 -> x^+m >= 1.
proof: Proof. elim => [|m ihm] x hx; first by rewrite expr0 lexx. apply: le_trans (hx) _ => /=; rewrite exprS. rewrite ler_pmulr; first exact: ihm. apply: lt_le_trans hx; exact: ltr01. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc