- improved fqu allows to prove fqu_cpx_trans and its derivatives

[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 dad1f938241812ef41928b983c6cb984f5ae5f2d..2c6ad2a5623d947abd287fa3e1ceccddb880087b 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.
 
 (* Inversion & forward lemmas ***********************************************)
 
+lemma nat_split: ∀x. x = 0 ∨ ∃y. ⫯y = x.
+* /3 width=2 by ex_intro, or_introl, or_intror/
+qed-.
+
 lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
 /4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
 qed-.