Bounds on specific values of the exponential

theorem Real.exp_one_near_10 : |Real.exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10

theorem Real.exp_one_near_20 : |Real.exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20

theorem Real.exp_one_gt_d9 : 2.7182818283 < Real.exp 1

theorem Real.exp_one_lt_d9 : Real.exp 1 < 2.7182818286

theorem Real.exp_neg_one_gt_d9 : 0.36787944116 < Real.exp (-1)

theorem Real.exp_neg_one_lt_d9 : Real.exp (-1) < 0.3678794412

theorem Real.log_two_near_10 : |Real.log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

theorem Real.log_two_gt_d9 : 0.6931471803 < Real.log 2

theorem Real.log_two_lt_d9 : Real.log 2 < 0.6931471808