proposition: Lemma cos_increasing_1 : forall x y:R, PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x < y -> cos x < cos y.
proof: Proof. intros x y H1 H2 H3 H4 H5; generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1); generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2); generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3); generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4); generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5); rewrite <- (cos_neg x); rewrite <- (cos_neg y); rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring. replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring. replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field. replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field. clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5; replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field. replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field. repeat rewrite cos_shift; apply (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg