X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_pred_succ.ma;h=3d79e371ebb0561e12510868a5af77df236c3868;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=ac01f0f8fc3aefbf78466e018ea478e8db5840f4;hpb=19b0a814861157ba05f23877d5cd94059f52c2e8;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma index ac01f0f8f..3d79e371e 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma @@ -24,10 +24,10 @@ lemma npred_succ (n): n = ↓↑n. * // qed. -(* Inversion with nsucc *****************************************************) +(* Inversions with nsucc ****************************************************) (*** nat_split *) -lemma nat_split (n): ∨∨ 𝟎 = n | n = ↑↓n. +lemma nat_split_zero_pos (n): ∨∨ 𝟎 = n | n = ↑↓n. #n @(nat_ind_succ … n) -n /2 width=1 by or_introl, or_intror/ qed-.