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