]> matita.cs.unibo.it Git - helm.git/commitdiff
goal ==> focus
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 24 Apr 2007 15:06:19 +0000 (15:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 24 Apr 2007 15:06:19 +0000 (15:06 +0000)
helm/software/matita/library_auto/auto/nat/div_and_mod.ma

index 9b9be7cf2518b090461fdb1b6911238f3fff2c15..215f387af0ec11951a85a54e456072c673d5fab6 100644 (file)
@@ -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.