proposition: Lemma powR1 : powR 1 = fun=> 1.
proof: Proof. by apply/funext => x; rewrite /powR oner_eq0 ln1 mulr0 expR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex