clear H.
= (x \sup m + m · (x \sup (1 + pred m))) by _.
= (x \sup m + m · x \sup m) by _.
- = ((1+m) · x \sup m) by _ (timeout=60)
+ = ((1+m) · x \sup m) by _ (timeout=120)
done.
qed.
= (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _.
= (x \sup (1+m) · (costante (2 + m))) by _
done.
-qed.
\ No newline at end of file
+qed.