- (D[x \sup (1+m)])
- = (D[x · x \sup m]).
- = (D[x] · x \sup m + x · D[x \sup m]).
- = (x \sup m + x · (m · x \sup (pred m))) timeout=30.
- = (x \sup m + m · (x \sup (1 + pred m))).
- = (x \sup m + m · x \sup m).
- = ((1+m) · x \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
+ (D[X \sup (1+m)])
+ = (D[X · X \sup m]).
+ = (D[X] · X \sup m + X · D[X \sup m]).
+ = (X \sup m + X · (m · X \sup (pred m))).
+ lapply depth=0 Fmult_associative;
+ lapply depth=0 Fmult_commutative;
+ = (X \sup m + m · (X · X \sup (pred m))) by Fmult_associative, Fmult_commutative.
+ = (X \sup m + m · (X \sup (1 + pred m))).
+ = (X \sup m + m · X \sup m).
+ = ((1+m) · X \sup m) by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum