proposition: Lemma ArTanH_series_coef_lemma : forall (R:COrdField) n, Nat.Odd n -> (nring (R:=R) n)[#][0].
proof: Proof. intros R [|n] H%Nat.odd_spec; [discriminate H |]. apply nringS_ap_zero. Qed.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac