fact: Definition ArTanH_series_coef (n:nat) := match (CLogic.Even_Odd_dec n) with | left _ => [0] | right H => [1][/](nring n)[//](ArTanH_series_coef_lemma IR n H) end.
imports: CoRN.transc.Exponential CoRN.tactics.CornTac