proposition: Lemma scale_exists x : x > 0 -> exists s, exp2R s * x > 1.
proof: Proof. move=> Hx; have [[s|s'] [_]] := find_range1z x^-1; last first. case; apply: ltRW; apply: leR_lt_trans (invR_gt0 Hx). by rewrite NegzE addRC intRN -leR_opp2 oppR0 oppRB -intRB1; apply: leR0n. rewrite -intRS -/intRR -(leR_pmul2l _ _ Hx) (divRR (gtR_neq Hx)) mulRC => Hs. exists s; apply: ltR_le_trans Hs _; rewrite leR_pmul2r {x Hx}//. by apply/intR_leP; rewrite lez_nat ltn_expl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)