proposition: Lemma expf_gt1 : forall m (x : F), x > 1 -> x^+m.+1 > 1.
proof: Proof. elim => [|m ihm] x hx; first by rewrite expr1. apply: lt_trans (hx) _ => /=; rewrite exprS -{1}(mulr1 x). rewrite ltr_pmul2l; first exact: ihm. apply: lt_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