arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_le_minus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
index 607a9135ef31308662bb9003febd8d85bd51a5e5..5656acffd1c61acc1eb9a4618f91a057f12d8370 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus.ma
@@ -21,7 +21,7 @@ include "ground/arith/nat_le_pred.ma".
 
 (*** minus_le *)
 lemma nle_minus_sn_refl_sn (m) (n): m - n ≤ m.
-#m #n elim n -n //
+#m #n @(nat_ind_succ … n) -n //
 #n #IH /2 width=3 by nle_trans/
 qed.
 
@@ -30,13 +30,13 @@ lemma nle_minus_succ_sn (m) (n): ↑n - m ≤ ↑(n - m).
 
 (*** inv_eq_minus_O *)
 lemma nle_eq_minus_O (m) (n): 𝟎 = m - n → m ≤ n.
-#m #n @(nat_ind_2 … m n) //
+#m #n @(nat_ind_succ_2 … m n) //
 /3 width=1 by nle_succ_bi/
 qed.
 
 (*** monotonic_le_minus_l *)
 lemma nle_minus_sn_bi (m) (n) (o): m ≤ n → m-o ≤ n-o.
-#m #n #o elim o -o //
+#m #n #o @(nat_ind_succ … o) -o //
 #o #IH #Hmn /3 width=1 by nle_pred_bi/
 qed.