Merge PR #13039: Lint stdlib with -mangle-names #3

Reviewed-by: anton-trunov

10 files changed, 71 insertions, 67 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 1db3f87cac..74d1e391c4 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -110,7 +110,7 @@ Section Between.
   Lemma between_in_int :
     forall k l, between k l -> forall r, in_int k l r -> P r.
   Proof.
-    induction 1; intros.
+    intro k; induction 1 as [|l]; intros r ?.
     - absurd (k < k). { auto with arith. }
       eapply in_int_lt; eassumption.
     - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith.
@@ -125,7 +125,7 @@ Section Between.
   Lemma exists_in_int :
     forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m.
   Proof.
-    induction 1 as [* ? (p, ?, ?)|].
+    induction 1 as [* ? (p, ?, ?)|l].
     - exists p; auto with arith.
     - exists l; auto with arith.
   Qed.
@@ -154,7 +154,7 @@ Section Between.
       between k l ->
       (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
   Proof.
-    induction 1; red; intros.
+    intro k; induction 1 as [|l]; red; intros.
     - absurd (k < k); auto with arith.
     - absurd (Q l). { auto with arith. }
       destruct (exists_in_int k (S l)) as (l',[],?).
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 341dd7de5d..1afc49b7ff 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -21,7 +21,7 @@ Defined.
 
 Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
 Proof.
-  induction n in m |- *; destruct m; auto with arith.
+  induction n as [|n IHn] in m |- *; destruct m as [|m]; auto with arith.
   destruct (IHn m) as [H|H]; auto with arith.
   destruct H; auto with arith.
 Defined.
@@ -33,9 +33,9 @@ Defined.
 
 Definition le_lt_dec n m : {n <= m} + {m < n}.
 Proof.
-  induction n in m |- *.
+  induction n as [|n IHn] in m |- *.
   - left; auto with arith.
-  - destruct m.
+  - destruct m as [|m].
     + right; auto with arith.
     + elim (IHn m); [left|right]; auto with arith.
 Defined.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 62a0f0a0ae..593d8c5934 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -34,7 +34,7 @@ Hint Resolve eq_nat_refl: arith.
 Theorem eq_nat_is_eq n m : eq_nat n m <-> n = m.
 Proof.
   split.
-  - revert m; induction n; destruct m; simpl; contradiction || auto.
+  - revert m; induction n; intro m; destruct m; simpl; contradiction || auto.
   - intros <-; apply eq_nat_refl.
 Qed.
 
@@ -53,12 +53,12 @@ Hint Immediate eq_eq_nat eq_nat_eq: arith.
 Theorem eq_nat_elim :
   forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
 Proof.
-  intros; replace m with n; auto with arith.
+  intros n P ? m ?; replace m with n; auto with arith.
 Qed.
 
 Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
 Proof.
-  induction n; destruct m; simpl.
+  intro n; induction n as [|n IHn]; intro m; destruct m; simpl.
   - left; trivial.
   - right; intro; trivial.
   - right; intro; trivial.
@@ -96,7 +96,7 @@ Qed.
 
 Definition beq_nat_eq : forall n m, true = (n =? m) -> n = m.
 Proof.
-  induction n; destruct m; simpl.
+  intro n; induction n as [|n IHn]; intro m; destruct m; simpl.
   - reflexivity.
   - discriminate.
   - discriminate.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 0871c4af67..f87d7e810a 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -33,7 +33,7 @@ Qed.
 
 Lemma fact_le n m : n <= m -> fact n <= fact m.
 Proof.
-  induction 1.
+  induction 1 as [|m ?].
   - apply le_n.
   - simpl. transitivity (fact m). trivial. apply Nat.le_add_r.
 Qed.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 4f17a7a8d3..4e71465452 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -80,7 +80,7 @@ Lemma le_elim_rel :
    (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
    forall n m, n <= m -> P n m.
 Proof.
-  intros P H0 HS.
+  intros P H0 HS n.
   induction n; trivial.
   intros m Le. elim Le; auto with arith.
  Qed.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 507d956e81..d7f703e6e4 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -158,7 +158,7 @@ Fixpoint mult_acc (s:nat) m n : nat :=
 
 Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
-  induction n as [| n IHn]; simpl; auto.
+  intro n; induction n as [| n IHn]; simpl; auto.
   intros. rewrite Nat.add_assoc, IHn. f_equal.
   rewrite Nat.add_comm. apply plus_tail_plus.
 Qed.
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
index 6f5339227a..37704704a0 100644
--- a/theories/Arith/PeanoNat.v
+++ b/theories/Arith/PeanoNat.v
@@ -75,7 +75,9 @@ Theorem recursion_succ :
     Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 Proof.
-unfold Proper, respectful in *; induction n; simpl; auto.
+unfold Proper, respectful in *.
+intros A Aeq a f ? ? n.
+induction n; simpl; auto.
 Qed.
 
 (** ** Remaining constants not defined in Coq.Init.Nat *)
@@ -126,7 +128,7 @@ Qed.
 
 Lemma sub_succ_r n m : n - (S m) = pred (n - m).
 Proof.
-revert m. induction n; destruct m; simpl; auto. apply sub_0_r.
+revert m. induction n; intro m; destruct m; simpl; auto. apply sub_0_r.
 Qed.
 
 Lemma mul_0_l n : 0 * n = 0.
@@ -136,9 +138,9 @@ Qed.
 
 Lemma mul_succ_l n m : S n * m = n * m + m.
 Proof.
-assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x.
+assert (succ_r : forall x y, x+S y = S(x+y)) by now intro x; induction x.
 assert (comm : forall x y, x+y = y+x).
-{ induction x; simpl; auto. intros; rewrite succ_r; now f_equal. }
+{ intro x; induction x; simpl; auto. intros; rewrite succ_r; now f_equal. }
 now rewrite comm.
 Qed.
 
@@ -152,7 +154,7 @@ Qed.
 Lemma eqb_eq n m : eqb n m = true <-> n = m.
 Proof.
  revert m.
- induction n; destruct m; simpl; rewrite ?IHn; split; try easy.
+ induction n as [|n IHn]; intro m; destruct m; simpl; rewrite ?IHn; split; try easy.
  - now intros ->.
  - now injection 1.
 Qed.
@@ -160,7 +162,7 @@ Qed.
 Lemma leb_le n m : (n <=? m) = true <-> n <= m.
 Proof.
  revert m.
- induction n; destruct m; simpl.
+ induction n as [|n IHn]; intro m; destruct m; simpl.
  - now split.
  - split; trivial. intros; apply Peano.le_0_n.
  - now split.
@@ -178,7 +180,7 @@ Qed.
 
 Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.
 Proof.
-  induction n; destruct m.
+  intro n; induction n as [|n IHn]; intro m; destruct m as [|m].
   - now left.
   - now right.
   - now right.
@@ -193,12 +195,14 @@ Defined.
 
 Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
 Proof.
- revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy.
+ revert m; induction n as [|n IHn]; intro m; destruct m;
+ simpl; rewrite ?IHn; split; auto; easy.
 Qed.
 
 Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
 Proof.
- revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy.
+ revert m; induction n as [|n IHn]; intro m; destruct m;
+ simpl; rewrite ?IHn; split; try easy.
  - intros _. apply Peano.le_n_S, Peano.le_0_n.
  - apply Peano.le_n_S.
  - apply Peano.le_S_n.
@@ -206,7 +210,7 @@ Qed.
 
 Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
 Proof.
- revert m; induction n; destruct m; simpl; rewrite ?IHn.
+ revert m; induction n as [|n IHn]; intro m; destruct m; simpl; rewrite ?IHn.
  - now split.
  - split; intros. apply Peano.le_0_n. easy.
  - split. now destruct 1. inversion 1.
@@ -215,7 +219,7 @@ Qed.
 
 Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
 Proof.
- revert m; induction n; destruct m; simpl; trivial.
+ revert m; induction n; intro m; destruct m; simpl; trivial.
 Qed.
 
 Lemma compare_succ n m : (S n ?= S m) = (n ?= m).
@@ -292,7 +296,7 @@ Lemma Even_2 n : Even n <-> Even (S (S n)).
 Proof.
  split; intros (m,H).
  - exists (S m). rewrite H. simpl. now rewrite plus_n_Sm.
- - destruct m; try discriminate.
+ - destruct m as [|m]; try discriminate.
    exists m. simpl in H. rewrite <- plus_n_Sm in H. now inversion H.
 Qed.
 
@@ -305,7 +309,7 @@ Lemma Odd_2 n : Odd n <-> Odd (S (S n)).
 Proof.
  split; intros (m,H).
  - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m).
- - destruct m; try discriminate.
+ - destruct m as [|m]; try discriminate.
    exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H.
    simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O.
 Qed.
@@ -316,7 +320,7 @@ Import Private_Parity.
 Lemma even_spec : forall n, even n = true <-> Even n.
 Proof.
  fix even_spec 1.
-  destruct n as [|[|n]]; simpl.
+  intro n; destruct n as [|[|n]]; simpl.
   - split; [ now exists 0 | trivial ].
   - split; [ discriminate | intro H; elim (Even_1 H) ].
   - rewrite even_spec. apply Even_2.
@@ -326,7 +330,7 @@ Lemma odd_spec : forall n, odd n = true <-> Odd n.
 Proof.
  unfold odd.
  fix odd_spec 1.
-  destruct n as [|[|n]]; simpl.
+  intro n; destruct n as [|[|n]]; simpl.
   - split; [ discriminate | intro H; elim (Odd_0 H) ].
   - split; [ now exists 0 | trivial ].
   - rewrite odd_spec. apply Odd_2.
@@ -338,9 +342,9 @@ Lemma divmod_spec : forall x y q u, u <= y ->
  let (q',u') := divmod x y q u in
  x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.
 Proof.
- induction x.
+ intro x; induction x as [|x IHx].
  - simpl; intuition.
- - intros y q u H. destruct u; simpl divmod.
+ - intros y q u H. destruct u as [|u]; simpl divmod.
    + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u').
      intros (EQ,LE); split; trivial.
      rewrite <- EQ, sub_0_r, sub_diag, add_0_r.
@@ -356,7 +360,7 @@ Qed.
 Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y.
 Proof.
  intros Hy.
- destruct y; [ now elim Hy | clear Hy ].
+ destruct y as [|y]; [ now elim Hy | clear Hy ].
  unfold div, modulo.
  generalize (divmod_spec x y 0 y (le_n y)).
  destruct divmod as (q,u).
@@ -380,7 +384,7 @@ Lemma sqrt_iter_spec : forall k p q r,
  let s := sqrt_iter k p q r in
  s*s <= k + p*p + (q - r) < (S s)*(S s).
 Proof.
- induction k.
+ intro k; induction k as [|k IHk].
  - (* k = 0 *)
    simpl; intros p q r Hq Hr.
    split.
@@ -391,7 +395,7 @@ Proof.
      apply add_le_mono_l.
      rewrite <- Hq. apply le_sub_l.
  - (* k = S k' *)
-   destruct r.
+   intros p q r; destruct r as [|r].
    + (* r = 0 *)
      intros Hq _.
      replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))).
@@ -427,7 +431,7 @@ Lemma log2_iter_spec : forall k p q r,
  let s := log2_iter k p q r in
  2^s <= k + q < 2^(S s).
 Proof.
- induction k.
+ intro k; induction k as [|k IHk].
  - (* k = 0 *)
    intros p q r EQ LT. simpl log2_iter. cbv zeta.
    split.
@@ -438,7 +442,7 @@ Proof.
    + rewrite EQ, add_comm. apply add_lt_mono_l.
      apply lt_succ_r, le_0_l.
  - (* k = S k' *)
-   intros p q r EQ LT. destruct r.
+   intros p q r EQ LT. destruct r as [|r].
    + (* r = 0 *)
      rewrite add_succ_r, add_0_r in EQ.
      rewrite add_succ_l, <- add_succ_r. apply IHk.
@@ -537,7 +541,7 @@ Lemma le_div2 n : div2 (S n) <= n.
 Proof.
  revert n.
  fix le_div2 1.
- destruct n; simpl; trivial. apply lt_succ_r.
+ intro n; destruct n as [|n]; simpl; trivial. apply lt_succ_r.
  destruct n; [simpl|]; trivial. now constructor.
 Qed.
 
@@ -550,7 +554,7 @@ Qed.
 
 Lemma div2_decr a n : a <= S n -> div2 a <= n.
 Proof.
- destruct a; intros H.
+ destruct a as [|a]; intros H.
  - simpl. apply le_0_l.
  - apply succ_le_mono in H.
    apply le_trans with a; [ apply le_div2 | trivial ].
@@ -563,7 +567,7 @@ Qed.
 
 Lemma testbit_0_l : forall n, testbit 0 n = false.
 Proof.
- now induction n.
+ now intro n; induction n.
 Qed.
 
 Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
@@ -592,7 +596,7 @@ Qed.
 Lemma shiftr_specif : forall a n m,
  testbit (shiftr a n) m = testbit a (m+n).
 Proof.
- induction n; intros m. trivial.
+ intros a n; induction n as [|n IHn]; intros m. trivial.
  now rewrite add_0_r.
  now rewrite add_succ_r, <- add_succ_l, <- IHn.
 Qed.
@@ -600,7 +604,7 @@ Qed.
 Lemma shiftl_specif_high : forall a n m, n<=m ->
  testbit (shiftl a n) m = testbit a (m-n).
 Proof.
- induction n; intros m H. trivial.
+ intros a n; induction n as [|n IHn]; intros m H. trivial.
  now rewrite sub_0_r.
  destruct m. inversion H.
  simpl. apply succ_le_mono in H.
@@ -611,7 +615,7 @@ Qed.
 Lemma shiftl_spec_low : forall a n m, m<n ->
  testbit (shiftl a n) m = false.
 Proof.
- induction n; intros m H. inversion H.
+ intros a n; induction n as [|n IHn]; intros m H. inversion H.
  change (shiftl a (S n)) with (double (shiftl a n)).
  destruct m; simpl.
  unfold odd. apply negb_false_iff.
@@ -623,7 +627,7 @@ Qed.
 Lemma div2_bitwise : forall op n a b,
  div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
 Proof.
- intros. unfold bitwise; fold bitwise.
+ intros op n a b. unfold bitwise; fold bitwise.
  destruct (op (odd a) (odd b)).
  now rewrite div2_succ_double.
  now rewrite add_0_l, div2_double.
@@ -632,7 +636,7 @@ Qed.
 Lemma odd_bitwise : forall op n a b,
  odd (bitwise op (S n) a b) = op (odd a) (odd b).
 Proof.
- intros. unfold bitwise; fold bitwise.
+ intros op n a b. unfold bitwise; fold bitwise.
  destruct (op (odd a) (odd b)).
  apply odd_spec. rewrite add_comm. eexists; eauto.
  unfold odd. apply negb_false_iff. apply even_spec.
@@ -644,7 +648,7 @@ Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
  testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
 Proof.
  intros op Hop.
- induction n; intros m a b Ha.
+ intro n; induction n as [|n IHn]; intros m a b Ha.
  simpl. inversion Ha; subst. now rewrite testbit_0_l.
  destruct m.
  apply odd_bitwise.
@@ -657,7 +661,7 @@ Lemma testbit_bitwise_2 : forall op, op false false = false ->
  testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
 Proof.
  intros op Hop.
- induction n; intros m a b Ha Hb.
+ intro n; induction n as [|n IHn]; intros m a b Ha Hb.
  simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l.
  destruct m.
  apply odd_bitwise.
@@ -682,11 +686,11 @@ Lemma lor_spec a b n :
 Proof.
  unfold lor. apply testbit_bitwise_2.
  - trivial.
- - destruct (compare_spec a b).
+ - destruct (compare_spec a b) as [H|H|H].
    + rewrite max_l; subst; trivial.
    + apply lt_le_incl in H. now rewrite max_r.
    + apply lt_le_incl in H. now rewrite max_l.
- - destruct (compare_spec a b).
+ - destruct (compare_spec a b) as [H|H|H].
    + rewrite max_r; subst; trivial.
    + apply lt_le_incl in H. now rewrite max_r.
    + apply lt_le_incl in H. now rewrite max_l.
@@ -697,11 +701,11 @@ Lemma lxor_spec a b n :
 Proof.
  unfold lxor. apply testbit_bitwise_2.
  - trivial.
- - destruct (compare_spec a b).
+ - destruct (compare_spec a b) as [H|H|H].
    + rewrite max_l; subst; trivial.
    + apply lt_le_incl in H. now rewrite max_r.
    + apply lt_le_incl in H. now rewrite max_l.
- - destruct (compare_spec a b).
+ - destruct (compare_spec a b) as [H|H|H].
    + rewrite max_r; subst; trivial.
    + apply lt_le_incl in H. now rewrite max_r.
    + apply lt_le_incl in H. now rewrite max_l.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index a673a1119f..9a7a397023 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -16,7 +16,7 @@ Implicit Types m n x y : nat.
 
 Theorem O_or_S n : {m : nat | S m = n} + {0 = n}.
 Proof.
-  induction n.
+  induction n as [|n IHn].
   - now right.
   - left; exists n; auto.
 Defined.
@@ -47,7 +47,7 @@ pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2).
   2: reflexivity.
 generalize def_n2; revert le_mn1 le_mn2.
 generalize n0 at 1 4 5 7; intros n1 le_mn1.
-destruct le_mn1; intros le_mn2; destruct le_mn2.
+destruct le_mn1 as [|? le_mn1]; intros le_mn2; destruct le_mn2 as [|? le_mn2].
 + now intros def_n0; rewrite (UIP_nat _ _ def_n0 eq_refl).
 + intros def_n0; generalize le_mn2; rewrite <-def_n0; intros le_mn0.
   now destruct (Nat.nle_succ_diag_l _ le_mn0).
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index ec7426e648..5da7738adc 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -156,7 +156,7 @@ Fixpoint tail_plus n m : nat :=
 
 Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
 Proof.
-induction n as [| n IHn]; simpl; auto.
+intro n; induction n as [| n IHn]; simpl; auto.
 intro m; rewrite <- IHn; simpl; auto.
 Qed.
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 3bfef93726..ebd909c1dc 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -27,8 +27,8 @@ Definition gtof (a b:A) := f b > f a.
 Theorem well_founded_ltof : well_founded ltof.
 Proof.
   assert (H : forall n (a:A), f a < n -> Acc ltof a).
-  { induction n.
-    - intros; absurd (f a < 0); auto with arith.
+  { intro n; induction n as [|n IHn].
+    - intros a Ha; absurd (f a < 0); auto with arith.
     - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb.
       apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. }
   intros a. apply (H (S (f a))). auto with arith.
@@ -69,8 +69,8 @@ Theorem induction_ltof1 :
 Proof.
   intros P F.
   assert (H : forall n (a:A), f a < n -> P a).
-  { induction n.
-    - intros; absurd (f a < 0); auto with arith.
+  { intro n; induction n as [|n IHn].
+    - intros a Ha; absurd (f a < 0); auto with arith.
     - intros a Ha. apply F. unfold ltof. intros b Hb.
       apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. }
   intros a. apply (H (S (f a))). auto with arith.
@@ -107,8 +107,8 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
   assert (H : forall n (a:A), f a < n -> Acc R a).
-  { induction n.
-    - intros; absurd (f a < 0); auto with arith.
+  { intro n; induction n as [|n IHn].
+    - intros a Ha; absurd (f a < 0); auto with arith.
     - intros a Ha. apply Acc_intro. intros b Hb.
       apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. }
   intros a. apply (H (S (f a))). auto with arith.
@@ -212,26 +212,26 @@ Section LT_WF_REL.
   Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
   Proof.
     intros x [n fxn]; generalize dependent x.
-    pattern n; apply lt_wf_ind; intros.
-    constructor; intros.
+    pattern n; apply lt_wf_ind; intros n0 H x fxn.
+    constructor; intros y H0.
     destruct (F_compat y x) as (x0,H1,H2); trivial.
     apply (H x0); auto.
   Qed.
 
   Theorem well_founded_inv_lt_rel_compat : well_founded R.
   Proof.
-    constructor; intros.
-    case (F_compat y a); trivial; intros.
+    intro a; constructor; intros y H.
+    case (F_compat y a); trivial; intros x **.
     apply acc_lt_rel; trivial.
     exists x; trivial.
   Qed.
 
 End LT_WF_REL.
 
-Lemma well_founded_inv_rel_inv_lt_rel :
-  forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
+Lemma well_founded_inv_rel_inv_lt_rel (A:Set) (F:A -> nat -> Prop) :
+  well_founded (inv_lt_rel A F).
 Proof.
-  intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
+  apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
 Qed.
 
 (** A constructive proof that any non empty decidable subset of
@@ -253,8 +253,8 @@ Proof.
   intros P Pdec (n0,HPn0).
   assert
     (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
-               \/ (forall n', P n' -> n<=n')).
-  { induction n.
+               \/ (forall n', P n' -> n<=n')) as H.
+  { intro n; induction n as [|n IHn].
     - right. intros. apply Nat.le_0_l.
     - destruct IHn as [(n' & IH1 & IH2)|IH].
       + left. exists n'; auto with arith.