X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_lminus.ma;h=04cd607c9b2269c4317007342b06b3c85983dc33;hp=15e58fd55809d51b2eee55ac68bc048d96ffc215;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3 diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma index 15e58fd55..04cd607c9 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma @@ -61,7 +61,7 @@ qed. (* Advanced constructions ***************************************************) -(* yminus_O1 *) +(*** yminus_O1 *) lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n. // qed.