proposition: Lemma cos_sin_seq : forall n : nat, cos_seq n [=] sin_seq (S n).
proof: Proof. intro. apply eq_symmetric_unfolded. 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 (x0 = x); [ intro | lia ]. rewrite H; algebra. exfalso; lia. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)