Numbers: some improvements in proofs

 - a ltac solve_proper which generalizes solve_predicate_wd and co
 - using le_elim is nicer that (apply le_lteq; destruct ...)
 - "apply ->" can now be "apply" most of the time.

 Benefit: NumPrelude is now almost empty

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 127 insertions, 152 deletions

diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 3aa6f41d3..fdec8ceb7 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -28,7 +28,7 @@ Theorem add_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply lt_trans with (m + p);
-[now apply -> add_lt_mono_r | now apply -> add_lt_mono_l].
+[now apply add_lt_mono_r | now apply add_lt_mono_l].
 Qed.
 
 Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
@@ -46,21 +46,21 @@ Theorem add_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
 Proof.
 intros n m p q H1 H2.
 apply le_trans with (m + p);
-[now apply -> add_le_mono_r | now apply -> add_le_mono_l].
+[now apply add_le_mono_r | now apply add_le_mono_l].
 Qed.
 
 Theorem add_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply lt_le_trans with (m + p);
-[now apply -> add_lt_mono_r | now apply -> add_le_mono_l].
+[now apply add_lt_mono_r | now apply add_le_mono_l].
 Qed.
 
 Theorem add_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply le_lt_trans with (m + p);
-[now apply -> add_le_mono_r | now apply -> add_lt_mono_l].
+[now apply add_le_mono_r | now apply add_lt_mono_l].
 Qed.
 
 Theorem add_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n + m.
@@ -154,7 +154,7 @@ Qed.
 
 Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p.
 Proof.
- intros n m H. apply le_ind with (4:=H). solve_predicate_wd.
+ intros n m H. apply le_ind with (4:=H). solve_proper.
  exists 0; nzsimpl; split; order.
  clear m H. intros m H (p & EQ & LE). exists (S p).
   split. nzsimpl. now apply succ_wd. now apply le_le_succ_r.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index a86fec3fd..7c7f43de0 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -48,7 +48,7 @@ Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
 Proof.
 intros; split.
 apply succ_inj.
-apply succ_wd.
+intros. now apply succ_wd.
 Qed.
 
 Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
@@ -61,7 +61,7 @@ left-inverse to the successor at this point *)
 
 Section CentralInduction.
 
-Variable A : predicate t.
+Variable A : t -> Prop.
 Hypothesis A_wd : Proper (eq==>iff) A.
 
 Theorem central_induction :
@@ -70,7 +70,7 @@ Theorem central_induction :
       forall n, A n.
 Proof.
 intros z Base Step; revert Base; pattern z; apply bi_induction.
-solve_predicate_wd.
+solve_proper.
 intro; now apply bi_induction.
 intro; pose proof (Step n); tauto.
 Qed.
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index 9c022646b..6788cd4e8 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder.
 (** Interface of a gcd function, then its specification on naturals *)
 
 Module Type Gcd (Import A : Typ).
- Parameters Inline gcd : t -> t -> t.
+ Parameter Inline gcd : t -> t -> t.
 End Gcd.
 
 Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A).
@@ -71,12 +71,12 @@ Lemma eq_mul_1_nonneg : forall n m,
  0<=n -> n*m == 1 -> n==1 /\ m==1.
 Proof.
  intros n m Hn H.
- apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ le_elim Hn.
  destruct (lt_ge_cases m 0) as [Hm|Hm].
  generalize (mul_pos_neg n m Hn Hm). order'.
- apply le_lteq in Hm. destruct Hm as [Hm|Hm].
+ le_elim Hm.
  apply le_succ_l in Hn. rewrite <- one_succ in Hn.
- apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ le_elim Hn.
  generalize (lt_1_mul_pos n m Hn Hm). order.
  rewrite <- Hn, mul_1_l in H. now split.
  rewrite <- Hm, mul_0_r in H. order'.
@@ -108,7 +108,7 @@ Lemma divide_antisym_nonneg : forall n m,
  0<=n -> 0<=m -> (n | m) -> (m | n) -> n == m.
 Proof.
  intros n m Hn Hm (q,Hq) (r,Hr).
- apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ le_elim Hn.
  destruct (lt_ge_cases q 0) as [Hq'|Hq'].
  generalize (mul_pos_neg n q Hn Hq'). order.
  rewrite <- Hq, <- mul_assoc in Hr.
@@ -175,7 +175,7 @@ Proof.
  rewrite <- Hq.
  destruct (lt_ge_cases q 0) as [Hq'|Hq'].
  generalize (mul_pos_neg n q Hn Hq'). order.
- apply le_lteq in Hq'. destruct Hq' as [Hq'|Hq'].
+ le_elim Hq'.
  rewrite <- (mul_1_r n) at 1. apply mul_le_mono_pos_l; trivial.
  now rewrite one_succ, le_succ_l.
  rewrite <- Hq', mul_0_r in Hq. order.
@@ -219,8 +219,8 @@ Lemma gcd_unique_alt : forall n m p, 0<=p ->
 Proof.
  intros n m p Hp H.
  apply gcd_unique; trivial.
- apply -> H. apply divide_refl.
- apply -> H. apply divide_refl.
+ apply H. apply divide_refl.
+ apply H. apply divide_refl.
  intros. apply H. now split.
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
index 6e1c2b3a1..a5aa6d8ac 100644
--- a/theories/Numbers/NatInt/NZLog.v
+++ b/theories/Numbers/NatInt/NZLog.v
@@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder NZPow.
 (** Interface of a log2 function, then its specification on naturals *)
 
 Module Type Log2 (Import A : Typ).
- Parameters Inline log2 : t -> t.
+ Parameter Inline log2 : t -> t.
 End Log2.
 
 Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A).
@@ -155,8 +155,7 @@ Lemma log2_pos : forall a, 1<a -> 0 < log2 a.
 Proof.
  intros a Ha.
  assert (Ha' : 0 < a) by order'.
- assert (H := log2_nonneg a). apply le_lteq in H.
-  destruct H; trivial.
+ assert (H := log2_nonneg a). le_elim H; trivial.
  generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order.
  intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order.
 Qed.
@@ -168,7 +167,7 @@ Proof.
  intros a. split; intros H.
  destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
  generalize (log2_pos a Ha); order.
- apply le_lteq in H; destruct H.
+ le_elim H.
  apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ.
  rewrite H. apply log2_1.
 Qed.
@@ -246,7 +245,7 @@ Qed.
 Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a.
 Proof.
  intros a Ha.
- apply le_lteq in Ha; destruct Ha as [Ha|Ha].
+ le_elim Ha.
  now apply lt_le_incl, log2_lt_lin.
  rewrite <- Ha, log2_nonpos; order.
 Qed.
@@ -269,8 +268,8 @@ Lemma log2_mul_above : forall a b, 0<=a -> 0<=b ->
  log2 (a*b) <= log2 a + log2 b + 1.
 Proof.
  intros a b Ha Hb.
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
- apply le_lteq in Hb. destruct Hb as [Hb|Hb].
+ le_elim Ha.
+ le_elim Hb.
  apply lt_succ_r.
  rewrite add_1_r, <- add_succ_r, <- add_succ_l.
  apply log2_lt_pow2; try order_pos.
@@ -432,11 +431,11 @@ Proof.
   apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order.
  assert (H' : log2 b <= log2 (a+b)).
   apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
- apply le_lteq in H. destruct H as [H|H].
+ le_elim H.
  apply lt_le_trans with (log2 (a+b) + log2 b).
   now apply add_lt_mono_r. now apply add_le_mono_l.
  rewrite <- H at 1. apply add_lt_mono_l.
- apply le_lteq in H'. destruct H' as [H'|H']. trivial.
+ le_elim H'; trivial.
  symmetry in H. apply log2_same in H; try order_pos.
  symmetry in H'. apply log2_same in H'; try order_pos.
  revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order.
@@ -534,7 +533,7 @@ Qed.
 Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a.
 Proof.
  intros a Ha.
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
+ le_elim Ha.
  apply log2_up_unique; trivial.
  split; try order.
  apply pow_lt_mono_r; try order'.
@@ -586,7 +585,7 @@ Lemma log2_log2_up_spec : forall a, 0<a ->
 Proof.
  intros a H. split.
  now apply log2_spec.
- rewrite <-le_succ_l, <-one_succ, le_lteq in H. destruct H as [H|H].
+ rewrite <-le_succ_l, <-one_succ in H. le_elim H.
  now apply log2_up_spec.
  now rewrite <-H, log2_up_1, pow_0_r.
 Qed.
@@ -693,7 +692,7 @@ Qed.
 Lemma log2_up_le_lin : forall a, 0<=a -> log2_up a <= a.
 Proof.
  intros a Ha.
- apply le_lteq in Ha; destruct Ha as [Ha|Ha].
+ le_elim Ha.
  now apply lt_le_incl, log2_up_lt_lin.
  rewrite <- Ha, log2_up_nonpos; order.
 Qed.
@@ -709,8 +708,8 @@ Proof.
  intros a b Ha Hb.
  assert (Ha':=log2_up_nonneg a).
  assert (Hb':=log2_up_nonneg b).
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
- apply le_lteq in Hb. destruct Hb as [Hb|Hb].
+ le_elim Ha.
+ le_elim Hb.
  apply log2_up_le_pow2; try order_pos.
  rewrite pow_add_r; trivial.
  apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'.
@@ -722,8 +721,8 @@ Lemma log2_up_mul_below : forall a b, 0<a -> 0<b ->
  log2_up a + log2_up b <= S (log2_up (a*b)).
 Proof.
  intros a b Ha Hb.
- rewrite <-le_succ_l, <-one_succ, le_lteq in Ha. destruct Ha as [Ha|Ha].
- rewrite <-le_succ_l, <-one_succ, le_lteq in Hb. destruct Hb as [Hb|Hb].
+ rewrite <-le_succ_l, <-one_succ in Ha. le_elim Ha.
+ rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb.
  assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial).
  assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial).
  rewrite <- (lt_succ_pred 0 (log2_up a)); trivial.
@@ -752,7 +751,7 @@ Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b ->
  log2_up (a*2^b) == b + log2_up a.
 Proof.
  intros a b Ha Hb.
- rewrite <- le_succ_l, <- one_succ, le_lteq in Ha. destruct Ha as [Ha|Ha].
+ rewrite <- le_succ_l, <- one_succ in Ha; le_elim Ha.
  apply log2_up_unique. apply add_nonneg_pos; trivial. now apply log2_up_pos.
  split.
  assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)).
@@ -876,11 +875,11 @@ Proof.
   apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order.
  assert (H' : log2_up b <= log2_up (a+b)).
   apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
- apply le_lteq in H. destruct H as [H|H].
+ le_elim H.
  apply lt_le_trans with (log2_up (a+b) + log2_up b).
   now apply add_lt_mono_r. now apply add_le_mono_l.
  rewrite <- H at 1. apply add_lt_mono_l.
- apply le_lteq in H'. destruct H' as [H'|H']. trivial.
+ le_elim H'. trivial.
  symmetry in H. apply log2_up_same in H; try order_pos.
  symmetry in H'. apply log2_up_same in H'; try order_pos.
  revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 323ecef1b..3cd78351d 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -24,17 +24,16 @@ Qed.
 
 Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m).
 Proof.
-nzord_induct p.
-intros n m H; false_hyp H lt_irrefl.
-intros p H IH n m H1. nzsimpl.
-le_elim H. assert (LR : forall n m, n < m -> p * n + n < p * m + m).
-intros n1 m1 H2. apply add_lt_mono; [now apply -> IH | assumption].
-split; [apply LR |]. intro H2. apply -> lt_dne; intro H3.
-apply <- le_ngt in H3. le_elim H3.
-apply lt_asymm in H2. apply H2. now apply LR.
-rewrite H3 in H2; false_hyp H2 lt_irrefl.
-rewrite <- H; now nzsimpl.
-intros p H1 _ n m H2. destruct (lt_asymm _ _ H1 H2).
+intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). solve_proper.
+intros. now nzsimpl.
+clear p Hp. intros p Hp IH n m. nzsimpl.
+assert (LR : forall n m, n < m -> p * n + n < p * m + m)
+ by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH).
+split; intros H.
+now apply LR.
+destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
+rewrite EQ in H. order.
+apply LR in GT. order.
 Qed.
 
 Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p).
@@ -46,19 +45,19 @@ Qed.
 Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).
 Proof.
 nzord_induct p.
-intros n m H; false_hyp H lt_irrefl.
-intros p H1 _ n m H2. apply lt_succ_l in H2. apply <- nle_gt in H2.
-false_hyp H1 H2.
-intros p H IH n m H1. apply <- le_succ_l in H.
-le_elim H. assert (LR : forall n m, n < m -> p * m < p * n).
-intros n1 m1 H2. apply (le_lt_add_lt n1 m1).
-now apply lt_le_incl. rewrite <- 2 mul_succ_l. now apply -> IH.
-split; [apply LR |]. intro H2. apply -> lt_dne; intro H3.
-apply <- le_ngt in H3. le_elim H3.
-apply lt_asymm in H2. apply H2. now apply LR.
-rewrite H3 in H2; false_hyp H2 lt_irrefl.
-rewrite (mul_lt_pred p (S p)) by reflexivity.
-rewrite H; do 2 rewrite mul_0_l; now do 2 rewrite add_0_l.
+order.
+intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order.
+intros p Hp IH n m _. apply le_succ_l in Hp.
+le_elim Hp.
+assert (LR : forall n m, n < m -> p * m < p * n).
+ intros n1 m1 H. apply (le_lt_add_lt n1 m1).
+ now apply lt_le_incl. rewrite <- 2 mul_succ_l. now rewrite <- IH.
+split; intros H.
+now apply LR.
+destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
+rewrite EQ in H. order.
+apply LR in GT. order.
+rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl.
 Qed.
 
 Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p).
@@ -70,7 +69,7 @@ Qed.
 Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_pos_l.
+le_elim H2. apply lt_le_incl. now apply mul_lt_mono_pos_l.
 apply eq_le_incl; now rewrite H2.
 apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l.
 Qed.
@@ -78,7 +77,7 @@ Qed.
 Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_neg_l.
+le_elim H2. apply lt_le_incl. now apply mul_lt_mono_neg_l.
 apply eq_le_incl; now rewrite H2.
 apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l.
 Qed.
@@ -97,20 +96,13 @@ Qed.
 
 Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof.
-intros n m p H; split; intro H1.
-destruct (lt_trichotomy p 0) as [H2 | [H2 | H2]].
-apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * m < p * n); [now apply -> mul_lt_mono_neg_l |].
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-assert (H4 : p * n < p * m); [now apply -> mul_lt_mono_neg_l |].
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-false_hyp H2 H.
-apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m) by (now apply -> mul_lt_mono_pos_l).
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-assert (H4 : p * m < p * n) by (now apply -> mul_lt_mono_pos_l).
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-now rewrite H1.
+intros n m p Hp; split; intro H; [|now apply mul_wd].
+apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp];
+ destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
+apply (mul_lt_mono_neg_l p) in LT; order.
+apply (mul_lt_mono_neg_l p) in GT; order.
+apply (mul_lt_mono_pos_l p) in LT; order.
+apply (mul_lt_mono_pos_l p) in GT; order.
 Qed.
 
 Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m).
@@ -181,17 +173,17 @@ Qed.
 
 Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m.
 Proof.
-intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_pos_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_pos_r.
 Qed.
 
 Theorem mul_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m.
 Proof.
-intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r.
 Qed.
 
 Theorem mul_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r.
 Qed.
 
 Theorem mul_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0.
@@ -206,7 +198,7 @@ Qed.
 
 Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1.
+intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1.
 rewrite mul_1_l in H1. now apply lt_1_l with m.
 assumption.
 Qed.
@@ -227,7 +219,7 @@ Qed.
 Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof.
 intros n m; split; intro H.
-intro H1; apply -> eq_mul_0 in H1. tauto.
+intro H1; apply eq_mul_0 in H1. tauto.
 split; intro H1; rewrite H1 in H;
 (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H.
 Qed.
@@ -239,13 +231,13 @@ Qed.
 
 Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0.
 Proof.
-intros n m H1 H2. apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1].
 assumption. false_hyp H1 H2.
 Qed.
 
 Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0.
 Proof.
-intros n m H1 H2; apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1].
 false_hyp H1 H2. assumption.
 Qed.
 
@@ -281,18 +273,16 @@ Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m.
 Proof.
 intros n m H1 H2. destruct (lt_ge_cases n 0).
 now apply lt_le_trans with 0.
-destruct (lt_ge_cases n m).
-assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonneg.
-apply -> le_ngt in F. false_hyp H2 F.
+destruct (lt_ge_cases n m) as [LT|LE]; trivial.
+apply square_le_mono_nonneg in LE; order.
 Qed.
 
 Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m.
 Proof.
 intros n m H1 H2. destruct (lt_ge_cases n 0).
 apply lt_le_incl; now apply lt_le_trans with 0.
-destruct (le_gt_cases n m).
-assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg.
-apply -> lt_nge in F. false_hyp H2 F.
+destruct (le_gt_cases n m) as [LE|LT]; trivial.
+apply square_lt_mono_nonneg in LT; order.
 Qed.
 
 Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index ef9057c06..3722d4727 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -15,19 +15,19 @@ Module Type NZOrderProp
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
 Proof.
-intros n n' Hn m m' Hm. rewrite !lt_eq_cases, !Hn, !Hm; auto with *.
+intros n n' Hn m m' Hm. now rewrite <- !lt_succ_r, Hn, Hm.
 Qed.
 
 Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H].
 
 Theorem lt_le_incl : forall n m, n < m -> n <= m.
 Proof.
-intros; apply <- lt_eq_cases; now left.
+intros. apply lt_eq_cases. now left.
 Qed.
 
 Theorem le_refl : forall n, n <= n.
 Proof.
-intro; apply <- lt_eq_cases; now right.
+intro. apply lt_eq_cases. now right.
 Qed.
 
 Theorem lt_succ_diag_r : forall n, n < S n.
@@ -97,7 +97,7 @@ intros n m; nzinduct n m.
 intros H; false_hyp H lt_irrefl.
 intro n; split; intros H H1 H2.
 apply lt_succ_r in H2. le_elim H2.
-apply H; auto. apply -> le_succ_l. now apply lt_le_incl.
+apply H; auto. apply le_succ_l. now apply lt_le_incl.
 rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l.
 apply le_succ_l in H1. le_elim H1.
 apply H; auto. rewrite lt_succ_r. now apply lt_le_incl.
@@ -206,12 +206,12 @@ Qed.
 
 Theorem lt_succ_l : forall n m, S n < m -> n < m.
 Proof.
-intros n m H; apply -> le_succ_l; order.
+intros n m H; apply le_succ_l; order.
 Qed.
 
 Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m LE. rewrite <- lt_succ_r in LE. order.
+intros n m LE. apply lt_succ_r in LE. order.
 Qed.
 
 Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.
@@ -254,15 +254,14 @@ Proof.
 apply lt_le_incl, lt_0_2.
 Qed.
 
-Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
-Proof.
-intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order.
-Qed.
-
 (** The order tactic enriched with some knowledge of 0,1,2 *)
 
 Ltac order' := generalize lt_0_1 lt_1_2; order.
 
+Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
+Proof.
+intros n m H1 H2. rewrite <- le_succ_l, <- one_succ in H1. order.
+Qed.
 
 (** More Trichotomy, decidability and double negation elimination. *)
 
@@ -364,7 +363,7 @@ Proof.
 intro z; nzinduct n z.
 order.
 intro n; split; intros IH m H1 H2.
-apply -> le_succ_r in H2. destruct H2 as [H2 | H2].
+apply le_succ_r in H2. destruct H2 as [H2 | H2].
 now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2].
 apply IH. assumption. now apply le_le_succ_r.
 Qed.
@@ -414,14 +413,14 @@ Qed.
 Lemma rs'_rs'' : right_step' -> right_step''.
 Proof.
 intros RS' n; split; intros H1 m H2 H3.
-apply -> lt_succ_r in H3; le_elim H3;
+apply lt_succ_r in H3; le_elim H3;
 [now apply H1 | rewrite H3 in *; now apply RS'].
 apply H1; [assumption | now apply lt_lt_succ_r].
 Qed.
 
 Lemma rbase : A' z.
 Proof.
-intros m H1 H2. apply -> le_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply le_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n.
@@ -473,28 +472,28 @@ Let left_step'' := forall n, A' n <-> A' (S n).
 Lemma ls_ls' :  A z -> left_step -> left_step'.
 Proof.
 intros Az LS n H1 H2. le_elim H1.
-apply LS; trivial. apply H2; [now apply <- le_succ_l | now apply eq_le_incl].
+apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl].
 rewrite H1; apply Az.
 Qed.
 
 Lemma ls'_ls'' : left_step' -> left_step''.
 Proof.
 intros LS' n; split; intros H1 m H2 H3.
-apply -> le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
+apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
 le_elim H3.
-apply <- le_succ_l in H3. now apply H1.
+apply le_succ_l in H3. now apply H1.
 rewrite <- H3 in *; now apply LS'.
 Qed.
 
 Lemma lbase : A' (S z).
 Proof.
-intros m H1 H2. apply -> le_succ_l in H2.
-apply -> le_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply le_succ_l in H2.
+apply le_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := n); [assumption | now apply eq_le_incl].
+intros H1 n H2. apply (H1 n); [assumption | now apply eq_le_incl].
 Qed.
 
 Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.
@@ -551,8 +550,8 @@ Theorem order_induction' :
     forall n, A n.
 Proof.
 intros Az AS AP n; apply order_induction; try assumption.
-intros m H1 H2. apply AP in H2; [| now apply <- le_succ_l].
-apply -> (A_wd (P (S m)) m); [assumption | apply pred_succ].
+intros m H1 H2. apply AP in H2; [|now apply le_succ_l].
+now rewrite pred_succ in H2.
 Qed.
 
 End Center.
@@ -579,8 +578,8 @@ Theorem lt_ind : forall (n : t),
    forall m, n < m -> A m.
 Proof.
 intros n H1 H2 m H3.
-apply right_induction with (S n); [assumption | | now apply <- le_succ_l].
-intros; apply H2; try assumption. now apply -> le_succ_l.
+apply right_induction with (S n); [assumption | | now apply le_succ_l].
+intros; apply H2; try assumption. now apply le_succ_l.
 Qed.
 
 (** Elimination principle for <= *)
@@ -606,8 +605,8 @@ Section WF.
 
 Variable z : t.
 
-Let Rlt (n m : t) := z <= n /\ n < m.
-Let Rgt (n m : t) := m < n /\ n <= z.
+Let Rlt (n m : t) := z <= n < m.
+Let Rgt (n m : t) := m < n <= z.
 
 Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt.
 Proof.
@@ -619,25 +618,13 @@ Proof.
 intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
 Qed.
 
-Instance Acc_lt_wd : Proper (eq==>iff) (Acc Rlt).
-Proof.
-intros x1 x2 H; split; intro H1; destruct H1 as [H2];
-constructor; intros; apply H2; now (rewrite H || rewrite <- H).
-Qed.
-
-Instance Acc_gt_wd : Proper (eq==>iff) (Acc Rgt).
-Proof.
-intros x1 x2 H; split; intro H1; destruct H1 as [H2];
-constructor; intros; apply H2; now (rewrite H || rewrite <- H).
-Qed.
-
 Theorem lt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
 apply strong_right_induction' with (z := z).
-apply Acc_lt_wd.
+auto with typeclass_instances.
 intros n H; constructor; intros y [H1 H2].
-apply <- nle_gt in H2. elim H2. now apply le_trans with z.
+apply nle_gt in H2. elim H2. now apply le_trans with z.
 intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
@@ -645,11 +632,11 @@ Theorem gt_wf : well_founded Rgt.
 Proof.
 unfold well_founded.
 apply strong_left_induction' with (z := z).
-apply Acc_gt_wd.
+auto with typeclass_instances.
 intros n H; constructor; intros y [H1 H2].
-apply <- nle_gt in H2. elim H2. now apply le_lt_trans with n.
+apply nle_gt in H2. elim H2. now apply le_lt_trans with n.
 intros n H1 H2; constructor; intros m [H3 H4].
-apply H2. assumption. now apply <- le_succ_l.
+apply H2. assumption. now apply le_succ_l.
 Qed.
 
 End WF.
@@ -662,4 +649,3 @@ End NZOrderProp.
 Module NZOrderedType (NZ : NZDecOrdSig')
  <: DecidableTypeFull <: OrderedTypeFull
  := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
-
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 29b85724e..4287319e4 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -26,10 +26,10 @@ Module Type NZParityProp
 (** Morphisms *)
 
 Instance Even_wd : Proper (eq==>iff) Even.
-Proof. unfold Even. solve_predicate_wd. Qed.
+Proof. unfold Even. solve_proper. Qed.
 
 Instance Odd_wd : Proper (eq==>iff) Odd.
-Proof. unfold Odd. solve_predicate_wd. Qed.
+Proof. unfold Odd. solve_proper. Qed.
 
 Instance even_wd : Proper (eq==>Logic.eq) even.
 Proof.
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index 23c27777a..58704735f 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -69,7 +69,7 @@ Qed.
 
 Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.
 Proof.
- apply le_ind; intros. solve_predicate_wd.
+ apply le_ind; intros. solve_proper.
  now nzsimpl.
  now nzsimpl.
 Qed.
@@ -88,7 +88,7 @@ Hint Rewrite pow_2_r : nz.
 Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0.
 Proof.
  intros a b Hb. apply le_ind with (4:=Hb).
- solve_predicate_wd.
+ solve_proper.
  rewrite pow_0_r. order'.
  clear b Hb. intros b Hb IH.
  rewrite pow_succ_r by trivial.
@@ -118,7 +118,7 @@ Qed.
 Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->
   a^(b+c) == a^b * a^c.
 Proof.
- intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ intros a b c Hb. apply le_ind with (4:=Hb). solve_proper.
  now nzsimpl.
  clear b Hb. intros b Hb IH Hc.
  nzsimpl; trivial.
@@ -132,7 +132,7 @@ Proof.
  intros a b c.
  destruct (lt_ge_cases c 0) as [Hc|Hc].
  rewrite !(pow_neg_r _ _ Hc). now nzsimpl.
- apply le_ind with (4:=Hc). solve_predicate_wd.
+ apply le_ind with (4:=Hc). solve_proper.
  now nzsimpl.
  clear c Hc. intros c Hc IH.
  nzsimpl; trivial.
@@ -142,7 +142,7 @@ Qed.
 Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c ->
   a^(b*c) == (a^b)^c.
 Proof.
- intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ intros a b c Hb. apply le_ind with (4:=Hb). solve_proper.
  intros. now nzsimpl.
  clear b Hb. intros b Hb IH Hc.
  nzsimpl; trivial.
@@ -157,7 +157,7 @@ Proof.
  intros a b Ha.
  destruct (lt_ge_cases b 0) as [Hb|Hb].
  now rewrite !(pow_neg_r _ _ Hb).
- apply le_ind with (4:=Hb). solve_predicate_wd.
+ apply le_ind with (4:=Hb). solve_proper.
  nzsimpl; order'.
  clear b Hb. intros b Hb IH.
  nzsimpl; trivial. now apply mul_nonneg_nonneg.
@@ -165,7 +165,7 @@ Qed.
 
 Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b.
 Proof.
- intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper.
  nzsimpl; order'.
  clear b Hb. intros b Hb IH.
  nzsimpl; trivial. now apply mul_pos_pos.
@@ -175,7 +175,7 @@ Qed.
 
 Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c.
 Proof.
- intros a b c Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
+ intros a b c Hc. apply lt_ind with (4:=Hc). solve_proper.
  intros (Ha,H). nzsimpl; trivial; order.
  clear c Hc. intros c Hc IH (Ha,H).
  nzsimpl; try order.
@@ -327,7 +327,7 @@ Qed.
 
 Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b.
 Proof.
- intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper.
  nzsimpl. order'.
  clear b Hb. intros b Hb IH. nzsimpl; trivial.
  rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha.
@@ -347,7 +347,7 @@ Qed.
 Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c ->
   a^c + b^c <= (a+b)^c.
 Proof.
- intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
+ intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper.
  nzsimpl; order.
  clear c Hc. intros c Hc IH.
  assert (0<=c) by order'.
@@ -387,7 +387,7 @@ Proof.
   apply mul_le_mono_nonneg_l; trivial.
   apply pow_le_mono_l; try split; order.
  (* end *)
- intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
+ intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper.
  nzsimpl; order.
  clear c Hc. intros c Hc IH.
  assert (0<=c) by order.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 414770d18..8b6dcc3d6 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder.
 (** Interface of a sqrt function, then its specification on naturals *)
 
 Module Type Sqrt (Import A : Typ).
- Parameters Inline sqrt : t -> t.
+ Parameter Inline sqrt : t -> t.
 End Sqrt.
 
 Module Type SqrtNotation (A : Typ)(Import B : Sqrt A).
@@ -460,7 +460,7 @@ Qed.
 Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a.
 Proof.
  intros a Ha.
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
+ le_elim Ha.
  rewrite sqrt_up_eqn by (now apply mul_pos_pos).
  rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial.
  rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl.
@@ -516,7 +516,7 @@ Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)².
 Proof.
  intros a H. split.
  now apply sqrt_spec.
- rewrite le_lteq in H. destruct H as [H|H].
+ le_elim H.
  now apply sqrt_up_spec.
  now rewrite <-H, sqrt_up_0, mul_0_l.
 Qed.
@@ -596,7 +596,7 @@ Qed.
 Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a.
 Proof.
  intros a Ha.
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
+ le_elim Ha.
  rewrite sqrt_up_eqn; trivial. apply le_succ_l.
  apply le_lt_trans with (P a). apply sqrt_le_lin.
  now rewrite <- lt_succ_r, (lt_succ_pred 0).
@@ -670,7 +670,7 @@ Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a ->
 Proof.
  intros a Ha. split.
  intros EQ.
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
+ le_elim Ha.
  exists (√°a). split. apply sqrt_up_nonneg.
  generalize (proj2 (sqrt_up_spec a Ha)).
  assert (Ha' : 0 < S a) by (apply lt_succ_r; order').
@@ -710,8 +710,8 @@ Qed.
 Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)).
 Proof.
  intros a b Ha Hb.
- apply le_lteq in Ha; destruct Ha as [Ha|Ha].
- apply le_lteq in Hb; destruct Hb as [Hb|Hb].
+ le_elim Ha.
+ le_elim Hb.
  rewrite 3 sqrt_up_eqn; trivial.
  nzsimpl. rewrite <- 2 succ_le_mono.
  etransitivity; [eapply add_sqrt_le|].