X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Fdecidable.ma;h=d58996de307488cc24f3dc96e8e12fcbd57e42fc;hb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;hp=158d4d48a42b948ea86200c506ea977bd0fc1646;hpb=bb4f21cca72a36572dd7a97cf70f8a9eeafc4d6b;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index 158d4d48a..d58996de3 100644
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -109,7 +109,7 @@ intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
 
 lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
 intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
-apply (p2bT ? ? (lebP ? ?)); auto.
+apply (p2bT ? ? (lebP ? ?)); apply lt_to_le; assumption.
 qed. 
 
 definition ltb ≝ λx,y.leb (S x) y.
@@ -149,7 +149,8 @@ qed.
 
 
 (* OUT OF PLACE *)
-lemma ltW : ∀n,m. n < m → n < (S m). intros; auto. qed.
+lemma ltW : ∀n,m. n < m → n < (S m).
+intros; unfold lt; unfold lt in H; auto. qed.
 
 lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
 intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;