goal ==> focus

diff --git a/helm/software/matita/library_auto/auto/nat/div_and_mod.ma b/helm/software/matita/library_auto/auto/nat/div_and_mod.ma
index 9b9be7cf2518b090461fdb1b6911238f3fff2c15..215f387af0ec11951a85a54e456072c673d5fab6 100644 (file)
--- a/helm/software/matita/library_auto/auto/nat/div_and_mod.ma
+++ b/helm/software/matita/library_auto/auto/nat/div_and_mod.ma
@@ -261,9 +261,11 @@ qed.
 (* some properties of div and mod *)
 theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
 intros.
-apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
-goal 15. (* ?11 is closed with the following tactics *)
-apply div_mod_spec_div_mod.auto.auto.
+apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
+[2: apply div_mod_spec_div_mod.auto.
+| skip
+| auto
+]
 (*unfold lt.apply le_S_S.apply le_O_n.
 apply div_mod_spec_times.*)
 qed.