proposition: Lemma sin_cos_seq : forall n : nat, sin_seq n [=] [--] (cos_seq (S n)).
proof: Proof. intros. unfold sin_seq, cos_seq in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p; intros; simpl in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p0; intros; simpl in |- *. exfalso; lia. algebra. elim even_or_odd_plus; intros; simpl in |- *. elim p0; intros; simpl in |- *. cut (S x = x0); [ intro | lia ]. rewrite <- H; simpl in |- *; rational. exfalso; lia. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)