changelog to -rc-1

[helm.git] / matita / library / nat / minus.ma

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index f1178107a28d4f742a14942642b7daf650e97009..11585f2065706c33ba70901cd3944c4261ad775c 100644 (file)
--- 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.