proposition: Lemma exp_quo_plus r1 p1 q1 p2 q2 : (0 < q1)%N -> (0 < q2)%N -> 0 <= r1 -> exp_quo r1 (p1 * q2 + p2 * q1) (q1 * q2) = exp_quo r1 p1 q1 * exp_quo r1 p2 q2.
proof: Proof. move => Hq1pos Hq2pos Hr1pos. rewrite [LHS]exprD [in l in l * _ = _]mulnC !prod_root ?ler0q //. by rewrite mulnC exprM mulnC exprM !rootCK. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith