proposition: Theorem exp_lt_inv : forall x y:R, exp x < exp y -> x < y.
proof: Proof. intros x y H; case (Rtotal_order x y); [ intros H1 | intros [H1| H1] ]. - assumption. - rewrite H1 in H; elim (Rlt_irrefl _ H). - assert (H2 := exp_increasing _ _ H1). elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H2)). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra