proposition: Lemma tan_1_gt_1 : tan 1 > 1.
proof: Proof. assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); lra). assert (t1 : cos 1 <= 1 - 1/2 + 1/24). { destruct (pre_cos_bound 1 0) as [_ t]; try lra; revert t. unfold cos_approx, cos_term; simpl; intros t; apply Rle_trans with (1:=t). clear t; apply Req_le; field. } assert (t2 : 1 - 1/6 <= sin 1). { destruct (pre_sin_bound 1 0) as [t _]; try lra; revert t. unfold sin_approx, sin_term; simpl; intros t; apply Rle_trans with (2:=t). clear t; apply Req_le; field. } pattern 1 at 2; replace 1 with (cos 1 / cos 1) by (field; apply Rgt_not_eq; lra). apply Rlt_gt; apply (Rmult_lt_compat_r (/ cos 1) (cos 1) (sin 1)). { apply Rinv_0_lt_compat; assumption. } apply Rle_lt_trans with (1 := t1); apply Rlt_le_trans with (2 := t2). lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia