diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /theories/Arith/Peano_dec.v | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'theories/Arith/Peano_dec.v')
-rw-r--r-- | theories/Arith/Peano_dec.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 340a7968..f8020a50 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -38,8 +38,7 @@ intros m n. generalize (eq_refl (S n)). generalize n at -1. induction (S n) as [|n0 IHn0]; try discriminate. -clear n; intros n H; injection H; clear H; intro H. -rewrite <- H; intros le_mn1 le_mn2; clear n H. +clear n; intros n [= <-] le_mn1 le_mn2. pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2). 2: reflexivity. generalize def_n2; revert le_mn1 le_mn2. @@ -50,7 +49,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2. now destruct (Nat.nle_succ_diag_l _ le_mn0). + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). -+ intros def_n0; injection def_n0; intros ->. ++ intros def_n0. injection def_n0 as ->. rewrite (UIP_nat _ _ def_n0 eq_refl); simpl. assert (H : le_mn1 = le_mn2). now apply IHn0. |