- new component "s_transition" for the restored fqu and fquq

[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 3cb9e9f30967ccd92cce8af759037dcc5e22767e..f86f7a3bd75b1ca4532acfa39c2829a704335c9f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -172,6 +172,10 @@ qed-.
 lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
 /3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
 
+lemma succ_inv_refl_sn: ∀x. ⫯x = x → ⊥.
+#x #H @(lt_le_false x (⫯x)) //
+qed-.
+
 lemma lt_inv_O1: ∀n. 0 < n → ∃m. ⫯m = n.
 * /2 width=2 by ex_intro/
 #H cases (lt_le_false … H) -H //