https://github.com/math-comp/analysis/blob/7528cc1f76fb9f2edeb47e1fca81907ac5b8a81e/theories/derive.v#L1406 https://github.com/math-comp/analysis/blob/7528cc1f76fb9f2edeb47e1fca81907ac5b8a81e/theories/derive.v#L1415 https://github.com/math-comp/analysis/blob/7528cc1f76fb9f2edeb47e1fca81907ac5b8a81e/theories/derive.v#L1422 These three lines refer to derivation using GRing.exp but naming is inconsistent between them.