proposition: Theorem ln_lt_2 : / 2 < ln 2.
proof: Proof. apply Rmult_lt_reg_l with (r := 2). - prove_sup0. - rewrite Rinv_r. + apply exp_lt_inv. apply Rle_lt_trans with (1 := exp_le_3). change (3 < Rpower 2 (1 + 1)). repeat rewrite Rpower_plus; repeat rewrite Rpower_1. * now apply (IZR_lt 3 4). * prove_sup0. + discrR. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra