X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fetc%2Fynat%2Fynat_minus.etc;h=c8bd414d00b763816b6bd27550f38a4086903a07;hb=888840f6b3a71d3d686b53b702d362ab90ab0038;hp=a2f15a8e20b597af2d9275d338c691e7655e678c;hpb=19b0a814861157ba05f23877d5cd94059f52c2e8;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/etc/ynat/ynat_minus.etc b/matita/matita/contribs/lambdadelta/ground/etc/ynat/ynat_minus.etc index a2f15a8e2..c8bd414d0 100644 --- a/matita/matita/contribs/lambdadelta/ground/etc/ynat/ynat_minus.etc +++ b/matita/matita/contribs/lambdadelta/ground/etc/ynat/ynat_minus.etc @@ -225,3 +225,33 @@ lemma yle_inv_plus_inj_dx: ∀x,y:ynat. ∀z:nat. x + y ≤ z → #m #n #H1 #H2 #H3 destruct elim (yle_inv_plus_inj2 … Hz) -Hz /2 width=2 by ex4_2_intro/ qed-. + +(* Inversions with yplus ****************************************************) + +(*** yle_inv_plus_dx *) +lemma yle_inv_plus_dx (x) (y): + x ≤ y → ∃z. x + z = y. +#x #y * -x -y +[ #m #n #H + + @(ex_intro … (yinj (n-m))) (**) (* explicit constructor *) + /3 width=1 by plus_minus, eq_f/ +| /2 width=2 by ex_intro/ +] +qed-. + +lemma yle_inv_plus_sn: ∀x,y. x ≤ y → ∃z. z + x = y. +#x #y #H elim (yle_inv_plus_dx … H) -H +/2 width=2 by ex_intro/ +qed-. + +lemma ylt_inv_plus_sn: ∀x,y. x < y → ∃∃z. ↑z + x = y & x < ∞. +#x #y #H elim (ylt_inv_le … H) -H +#Hx #H elim (yle_inv_plus_sn … H) -H +/2 width=2 by ex2_intro/ +qed-. + +lemma ylt_inv_plus_dx: ∀x,y. x < y → ∃∃z. x + ↑z = y & x < ∞. +#x #y #H elim (ylt_inv_plus_sn … H) -H +#z >yplus_comm /2 width=2 by ex2_intro/ +qed-.