proposition: Lemma lt_cexp_pos : forall x y, (0 < y)%R -> (cexp x < cexp y)%Z -> (x < y)%R.
proof: Proof. intros x y Zy He. unfold cexp in He. apply (lt_mag beta) with (1 := Zy). generalize (monotone_exp (mag beta y) (mag beta x)). lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop