X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fminus.ma;h=11585f2065706c33ba70901cd3944c4261ad775c;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=f1178107a28d4f742a14942642b7daf650e97009;hpb=8e24e39aed25a2c31fb7073308ee3f0b80c206e6;p=helm.git

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index f1178107a..11585f206 100644
--- a/matita/library/nat/minus.ma
+++ b/matita/library/nat/minus.ma
@@ -287,6 +287,15 @@ rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
+theorem lt_O_minus_to_lt: \forall a,b:nat.
+O \lt b-a \to a \lt b.
+intros.
+rewrite > (plus_n_O a).
+rewrite > (sym_plus a O).
+apply (lt_minus_to_plus O  a b).
+assumption.
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.