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