(D[X \sup (1+m)] = (1+m) · X \sup m).
we need to prove
(m · (X \sup (1+ pred m)) = m · X \sup m) (Ppred).
+ lapply depth=0 le_n;
we proved (0 < m ∨ 0=m) (cases).
we proceed by induction on cases
to prove (m · (X \sup (1+ pred m)) = m · X \sup m).
(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 + 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) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
+ = ((1+m) · X \sup m) by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
done.
qed.