proposition: Lemma exp_quo_equiv r1 p1 q1 p2 q2 : (0 < q1)%N -> (0 < q2)%N -> 0 <= r1 -> (p1 * q2 = p2 * q1)%N -> exp_quo r1 p1 q1 = exp_quo r1 p2 q2.
proof: Proof. move => Hq1pos Hq2pos Hr1pos Heq. have Hprodpos : (0 < q1 * q2)%N by rewrite muln_gt0 Hq1pos Hq2pos. suff : q1.-root r1%:C ^+ p1 ^+ (q1 * q2) = q2.-root r1%:C ^+ p2 ^+ (q1 * q2). by apply: pexpIrn; rewrite // nnegrE exprn_ge0 ?rootC_ge0 ?ler0q. rewrite !exprM ![_ ^+ _ ^+ q1]exprAC -exprM ![_ ^+ _ ^+ q2]exprAC !rootCK //. by rewrite -exprM Heq mulnC. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith