proposition: Lemma exp_quo_self_grows (p1 q1 p2 q2 : nat) r1 r2 : (0 < q1)%N -> (0 < q2)%N -> r1 = p1%:Q / q1%:Q -> r2 = p2%:Q / q2%:Q -> 0 < r1 -> 1 <= r2 -> r1 <= r2 -> exp_quo r1 p1 q1 <= exp_quo r2 p2 q2.
proof: Proof. move => Hq1 Hq2 Hr1 Hr2 Hr1gt0 Hle1r2 Hle12. have Hr1pos : 0 <= r1 by apply: ltW. have Hr2pos : 0 <= r2 by rewrite Hr2 divr_ge0 // ?ler0z. have: r1%:C ^+ (p1 * q2) <= r2%:C ^+ (p1 * q2). by rewrite lerXn2r ?ler_rat // nnegrE ler0q. rewrite exp_quo_lessE // => /le_trans -> //; rewrite exp_incr_expp ?ler1q //. move: Hle12; rewrite Hr1 Hr2 ler_pdivrMr ?ltr0n //. by rewrite mulrAC ler_pdivlMr ?ltr0n // -!natrM ler_nat. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith