-apply (ltpow_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
-apply (lt_rewl ???? (zero_neutral ??));
-apply (lt_rewl ???? (zero_neutral ??));
-apply (lt_rewl ???? (powzero ?n1));
+apply (ltmul_lt ??? (S n1)); simplify; apply (Lt≫ ? f);
+apply (Lt≪ ? (zero_neutral ??)); (* bug se faccio repeat *)
+apply (Lt≪ ? (zero_neutral ??));
+apply (Lt≪ ? (mulzero ?n1));