X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=83322f4d8de57107b0eeb097bb7cd96d3cd83d86;hb=b6e1db4f1b0f1d5121f2b214562f96c5b0fa544e;hp=9fedf60c0c180fd43f5e2ce90139254ba59dbfca;hpb=0e2836b432e8d1a10262836e160a5dd3cfb82c1e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 9fedf60c0..83322f4d8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -158,6 +158,10 @@ qed.
 
 (* Inversion & forward lemmas ***********************************************)
 
+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-.
+
 lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
 /2 width=1 by plus_le_0/ qed-.