proposition: Lemma exp_quoMr r1 r2 p1 q1 (Hr2 : 0 <= r2) : exp_quo (r1 * r2) p1 q1 = exp_quo r1 p1 q1 * exp_quo r2 p1 q1.
proof: Proof. by rewrite mulrC exp_quoMl // mulrC. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith