proposition: Lemma exp_quo_gt0 r p q : (0 < q)%N -> (0 < r) -> 0 < exp_quo r p q.
proof: Proof. by move => Hq Hr; rewrite exprn_gte0 ?rootC_gt0 ?ltr0q. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith