proposition: Lemma exp_quo_lessE r1 r2 p1 q1 p2 q2 : 0 <= r1 -> 0 <= r2 -> (0 < q1)%N -> (0 < q2)%N -> (exp_quo r1 p1 q1 <= exp_quo r2 p2 q2) = (r1%:C ^+ (p1 * q2) <= r2%:C ^+ (p2 * q1)).
proof: Proof. move=> Hr1 Hr2 Hq1 Hq2; rewrite /exp_quo -!rootCX ?ler0q //. rewrite root_le_x // ?rootC_ge0 ?exprn_ge0 ?ler0q //. by rewrite -rootCX ?root_x_le ?exprn_ge0 ?ler0q // -!exprM. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith