some advances on reduction

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / arith.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 0cbcff85e6ce1daec44d6f56fe0f3b32ed52a322..832195fe90efcf4e404c39af1e6ed4f37eabd5ac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -52,6 +52,9 @@ lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
 
 (* Properties ***************************************************************)
 
+fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
 lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
 /3 width=1 by monotonic_le_minus_l/ qed.