proposition: Theorem lt_cexp : forall x y, (y <> 0)%R -> (cexp x < cexp y)%Z -> (Rabs x < Rabs y)%R.
proof: Proof. intros x y Zy He. apply lt_cexp_pos. now apply Rabs_pos_lt. now rewrite 2!cexp_abs. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop