X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fetc%2Flib%2Farith.etc;h=11ef739da890ce612a551e5556c118b53b04beac;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=1af2859d70e14f7e17e5469cbf3a217d3287bab9;hpb=67c5cf7ae14c745a94defbe645c5406ccbcf514d;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc index 1af2859d7..11ef739da 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc @@ -30,3 +30,7 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. #x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/ #Hxy elim (H Hxy) qed-. + +lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y. +#x #y #Hxy >minus_minus [|*: // ]