From 4e9f8c32689979faca3cfdc1692c1690fd789bfc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Apr 2007 15:06:19 +0000 Subject: [PATCH] goal ==> focus --- helm/software/matita/library_auto/auto/nat/div_and_mod.ma | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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 9b9be7cf2..215f387af 100644 --- 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. -- 2.39.2