proposition: Theorem exp_le_inv : forall x y : R, (exp x <= exp y)%R -> (x <= y)%R.
proof: Proof. intros x y H; case H; intros H2. left; apply exp_lt_inv; auto. right; apply exp_inv; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz