diff options
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. |