proposition: Lemma exp_quoMl r1 r2 p1 q1 (Hr1 : 0 <= r1) : exp_quo (r1 * r2) p1 q1 = exp_quo r1 p1 q1 * exp_quo r2 p1 q1.
proof: Proof. by rewrite /exp_quo rmorphM /= rootCMl ?exprMn ?ler0q. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith