proposition: Lemma exp_quo_gt1 r p q : (0 < p)%N -> (0 < q)%N -> 1 < r -> 1 < exp_quo r p q.
proof: Proof. by move => Hp Hq Hr; rewrite exprn_egt1 ?rootC_gt1 ?ltr1q -?lt0n. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith