proposition: Lemma sin_pi_seq_nonneg : forall n : nat, [0] [<=] Sin (pi_seq n).
proof: Proof. intro. astepl (Sin [0]). apply sin_pi_seq_mon with n. apply leEq_reflexive. apply pi_seq_nonneg. apply leEq_reflexive. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos