proposition: Lemma expRat_le_exp_exists : forall r d, ~ 1 <= r -> ~ d == 0 -> exists n, expRat r n <= d.
proof: Proof. intuition. destruct (expRat_half_le_exp_exists H0). destruct (expRat_le_half_exists H). exists (x0 * x)%nat. rewrite expRat_exp_prod. eapply leRat_trans. eapply expRat_leRat_compat. eapply H2. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms