proposition: Lemma prod_root m n x : (0 < m)%N -> (0 < n)%N -> 0 <= x -> (m * n)%N.-root x = m.-root (n.-root x).
proof: Proof. move => Hm Hn Hx. have Hmnpos : (0 < m * n)%N by rewrite muln_gt0 Hm Hn. suff: ((m * n).-root x) ^+ (m*n)%N = (m.-root (n.-root x)) ^+ (m * n)%N. by apply: pexpIrn; rewrite // nnegrE ?rootC_ge0 //. by rewrite rootCK // exprM rootCK // rootCK. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)