Merge PR #9386: Pass some files to strict focusing mode.

Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot

12 files changed, 1126 insertions, 1100 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index bc366c508d..9fcb029b3c 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -22,14 +22,16 @@ Ltac nzsimpl' := autorewrite with nz nz'.
 
 Theorem add_0_r : forall n, n + 0 == n.
 Proof.
-nzinduct n. now nzsimpl.
-intro. nzsimpl. now rewrite succ_inj_wd.
+  nzinduct n.
+  - now nzsimpl.
+  - intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
 Theorem add_succ_r : forall n m, n + S m == S (n + m).
 Proof.
-intros n m; nzinduct n. now nzsimpl.
-intro. nzsimpl. now rewrite succ_inj_wd.
+  intros n m; nzinduct n.
+  - now nzsimpl.
+  - intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
 Theorem add_succ_comm : forall n m, S n + m == n + S m.
@@ -41,8 +43,9 @@ Hint Rewrite add_0_r add_succ_r : nz.
 
 Theorem add_comm : forall n m, n + m == m + n.
 Proof.
-intros n m; nzinduct n. now nzsimpl.
-intro. nzsimpl. now rewrite succ_inj_wd.
+  intros n m; nzinduct n.
+  - now nzsimpl.
+  - intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
 Theorem add_1_l : forall n, 1 + n == S n.
@@ -59,14 +62,16 @@ Hint Rewrite add_1_l add_1_r : nz.
 
 Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
-intros n m p; nzinduct n. now nzsimpl.
-intro. nzsimpl. now rewrite succ_inj_wd.
+  intros n m p; nzinduct n.
+  - now nzsimpl.
+  - intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
 Theorem add_cancel_l : forall n m p, p + n == p + m <-> n == m.
 Proof.
-intros n m p; nzinduct p. now nzsimpl.
-intro p. nzsimpl. now rewrite succ_inj_wd.
+intros n m p; nzinduct p.
+- now nzsimpl.
+- intro p. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
 Theorem add_cancel_r : forall n m p, n + p == m + p <-> n == m.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 99812ee3fe..5f102e853b 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -17,8 +17,8 @@ Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
-intros n m p; nzinduct p. now nzsimpl.
-intro p. nzsimpl. now rewrite <- succ_lt_mono.
+  intros n m p; nzinduct p. - now nzsimpl.
+  - intro p. nzsimpl. now rewrite <- succ_lt_mono.
 Qed.
 
 Theorem add_lt_mono_r : forall n m p, n < m <-> n + p < m + p.
@@ -35,8 +35,8 @@ Qed.
 
 Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
 Proof.
-intros n m p; nzinduct p. now nzsimpl.
-intro p. nzsimpl. now rewrite <- succ_le_mono.
+  intros n m p; nzinduct p. - now nzsimpl.
+  - intro p. nzsimpl. now rewrite <- succ_le_mono.
 Qed.
 
 Theorem add_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.
@@ -124,9 +124,9 @@ Qed.
 Theorem add_le_cases : forall n m p q, n + m <= p + q -> n <= p \/ m <= q.
 Proof.
 intros n m p q H.
-destruct (le_gt_cases n p) as [H1 | H1]. now left.
-destruct (le_gt_cases m q) as [H2 | H2]. now right.
-contradict H; rewrite nle_gt. now apply add_lt_mono.
+destruct (le_gt_cases n p) as [H1 | H1]. - now left.
+- destruct (le_gt_cases m q) as [H2 | H2]. + now right.
+  + contradict H; rewrite nle_gt. now apply add_lt_mono.
 Qed.
 
 Theorem add_neg_cases : forall n m, n + m < 0 -> n < 0 \/ m < 0.
@@ -156,10 +156,10 @@ 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_proper.
- exists 0; nzsimpl; split; order.
- clear m H. intros m H (p & EQ & LE). exists (S p).
-  split. nzsimpl. now f_equiv. now apply le_le_succ_r.
+  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 f_equiv. + now apply le_le_succ_r.
 Qed.
 
 (** For the moment, it doesn't seem possible to relate
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 595b2182ab..840a798d9b 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -49,8 +49,8 @@ bidirectional induction steps *)
 Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
 Proof.
 intros; split.
-apply succ_inj.
-intros. now f_equiv.
+- apply succ_inj.
+- intros. now f_equiv.
 Qed.
 
 Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
@@ -72,9 +72,9 @@ Theorem central_induction :
       forall n, A n.
 Proof.
 intros z Base Step; revert Base; pattern z; apply bi_induction.
-solve_proper.
-intro; now apply bi_induction.
-intro; pose proof (Step n); tauto.
+- solve_proper.
+- intro; now apply bi_induction.
+- intro; pose proof (Step n); tauto.
 Qed.
 
 End CentralInduction.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 550aa226ac..b94cef7cee 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -54,22 +54,22 @@ Proof.
 intros b.
 assert (U : forall q1 q2 r1 r2,
             b*q1+r1 == b*q2+r2 -> 0<=r1<b -> 0<=r2 -> q1<q2 -> False).
- intros q1 q2 r1 r2 EQ LT Hr1 Hr2.
- contradict EQ.
- apply lt_neq.
- apply lt_le_trans with (b*q1+b).
- rewrite <- add_lt_mono_l. tauto.
- apply le_trans with (b*q2).
- rewrite mul_comm, <- mul_succ_l, mul_comm.
- apply mul_le_mono_nonneg_l; intuition; try order.
- rewrite le_succ_l; auto.
- rewrite <- (add_0_r (b*q2)) at 1.
- rewrite <- add_le_mono_l. tauto.
-
-intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]].
-elim (U q1 q2 r1 r2); intuition.
-split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto.
-elim (U q2 q1 r2 r1); intuition.
+- intros q1 q2 r1 r2 EQ LT Hr1 Hr2.
+  contradict EQ.
+  apply lt_neq.
+  apply lt_le_trans with (b*q1+b).
+  + rewrite <- add_lt_mono_l. tauto.
+  + apply le_trans with (b*q2).
+    * rewrite mul_comm, <- mul_succ_l, mul_comm.
+      apply mul_le_mono_nonneg_l; intuition; try order.
+      rewrite le_succ_l; auto.
+    * rewrite <- (add_0_r (b*q2)) at 1.
+      rewrite <- add_le_mono_l. tauto.
+
+- intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]].
+  + elim (U q1 q2 r1 r2); intuition.
+  + split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto.
+  + elim (U q2 q1 r2 r1); intuition.
 Qed.
 
 Theorem div_unique:
@@ -78,8 +78,8 @@ Theorem div_unique:
 Proof.
 intros a b q r Ha (Hb,Hr) EQ.
 destruct (div_mod_unique b q (a/b) r (a mod b)); auto.
-apply mod_bound_pos; order.
-rewrite <- div_mod; order.
+- apply mod_bound_pos; order.
+- rewrite <- div_mod; order.
 Qed.
 
 Theorem mod_unique:
@@ -88,8 +88,8 @@ Theorem mod_unique:
 Proof.
 intros a b q r Ha (Hb,Hr) EQ.
 destruct (div_mod_unique b q (a/b) r (a mod b)); auto.
-apply mod_bound_pos; order.
-rewrite <- div_mod; order.
+- apply mod_bound_pos; order.
+- rewrite <- div_mod; order.
 Qed.
 
 Theorem div_unique_exact a b q:
@@ -167,16 +167,16 @@ Qed.
 Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a.
 Proof.
 intros; symmetry. apply div_unique_exact; trivial.
-apply mul_nonneg_nonneg; order.
-apply mul_comm.
+- apply mul_nonneg_nonneg; order.
+- apply mul_comm.
 Qed.
 
 Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0.
 Proof.
 intros; symmetry.
 apply mod_unique with a; try split; try order.
-apply mul_nonneg_nonneg; order.
-nzsimpl; apply mul_comm.
+- apply mul_nonneg_nonneg; order.
+- nzsimpl; apply mul_comm.
 Qed.
 
 
@@ -187,10 +187,10 @@ Qed.
 Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.
 Proof.
 intros. destruct (le_gt_cases b a).
-apply le_trans with b; auto.
-apply lt_le_incl. destruct (mod_bound_pos a b); auto.
-rewrite lt_eq_cases; right.
-apply mod_small; auto.
+- apply le_trans with b; auto.
+  apply lt_le_incl. destruct (mod_bound_pos a b); auto.
+- rewrite lt_eq_cases; right.
+  apply mod_small; auto.
 Qed.
 
 
@@ -219,9 +219,9 @@ Qed.
 Lemma div_small_iff : forall a b, 0<=a -> 0<b -> (a/b==0 <-> a<b).
 Proof.
 intros a b Ha Hb; split; intros Hab.
-destruct (lt_ge_cases a b); auto.
-symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto.
-apply div_small; auto.
+- destruct (lt_ge_cases a b); auto.
+  symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto.
+- apply div_small; auto.
 Qed.
 
 Lemma mod_small_iff : forall a b, 0<=a -> 0<b -> (a mod b == a <-> a<b).
@@ -236,9 +236,9 @@ Qed.
 Lemma div_str_pos_iff : forall a b, 0<=a -> 0<b -> (0<a/b <-> b<=a).
 Proof.
 intros a b Ha Hb; split; intros Hab.
-destruct (lt_ge_cases a b) as [LT|LE]; auto.
-rewrite <- div_small_iff in LT; order.
-apply div_str_pos; auto.
+- destruct (lt_ge_cases a b) as [LT|LE]; auto.
+  rewrite <- div_small_iff in LT; order.
+- apply div_str_pos; auto.
 Qed.
 
 
@@ -250,14 +250,14 @@ Proof.
 intros.
 assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1).
 destruct (lt_ge_cases a b).
-rewrite div_small; try split; order.
-rewrite (div_mod a b) at 2 by order.
-apply lt_le_trans with (b*(a/b)).
-rewrite <- (mul_1_l (a/b)) at 1.
-rewrite <- mul_lt_mono_pos_r; auto.
-apply div_str_pos; auto.
-rewrite <- (add_0_r (b*(a/b))) at 1.
-rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
+- rewrite div_small; try split; order.
+- rewrite (div_mod a b) at 2 by order.
+  apply lt_le_trans with (b*(a/b)).
+  + rewrite <- (mul_1_l (a/b)) at 1.
+    rewrite <- mul_lt_mono_pos_r; auto.
+    apply div_str_pos; auto.
+  + rewrite <- (add_0_r (b*(a/b))) at 1.
+    rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
 Qed.
 
 (** [le] is compatible with a positive division. *)
@@ -276,8 +276,8 @@ apply lt_le_trans with b; auto.
 rewrite (div_mod b c) at 1 by order.
 rewrite <- add_assoc, <- add_le_mono_l.
 apply le_trans with (c+0).
-nzsimpl; destruct (mod_bound_pos b c); order.
-rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order.
+- nzsimpl; destruct (mod_bound_pos b c); order.
+- rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order.
 Qed.
 
 (** The following two properties could be used as specification of div *)
@@ -334,11 +334,11 @@ Theorem div_le_lower_bound:
 Proof.
 intros a b q Ha Hb H.
 destruct (lt_ge_cases 0 q).
-rewrite <- (div_mul q b); try order.
-apply div_le_mono; auto.
-rewrite mul_comm; split; auto.
-apply lt_le_incl, mul_pos_pos; auto.
-apply le_trans with 0; auto; apply div_pos; auto.
+- rewrite <- (div_mul q b); try order.
+  apply div_le_mono; auto.
+  rewrite mul_comm; split; auto.
+  apply lt_le_incl, mul_pos_pos; auto.
+- apply le_trans with 0; auto; apply div_pos; auto.
 Qed.
 
 (** A division respects opposite monotonicity for the divisor *)
@@ -350,10 +350,10 @@ Proof.
  apply div_le_lower_bound; auto.
  rewrite (div_mod p r) at 2 by order.
  apply le_trans with (r*(p/r)).
- apply mul_le_mono_nonneg_r; try order.
- apply div_pos; order.
- rewrite <- (add_0_r (r*(p/r))) at 1.
- rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order.
+ - apply mul_le_mono_nonneg_r; try order.
+   apply div_pos; order.
+ - rewrite <- (add_0_r (r*(p/r))) at 1.
+   rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order.
 Qed.
 
 
@@ -365,9 +365,9 @@ Proof.
  intros.
  symmetry.
  apply mod_unique with (a/c+b); auto.
- apply mod_bound_pos; auto.
- rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
- now rewrite mul_comm.
+ - apply mod_bound_pos; auto.
+ - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
+   now rewrite mul_comm.
 Qed.
 
 Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c ->
@@ -396,14 +396,14 @@ Proof.
  intros.
  symmetry.
  apply div_unique with ((a mod b)*c).
- apply mul_nonneg_nonneg; order.
- split.
- apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order.
- rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto.
- rewrite (div_mod a b) at 1 by order.
- rewrite mul_add_distr_r.
- rewrite add_cancel_r.
- rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
+ - apply mul_nonneg_nonneg; order.
+ - split.
+   + apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order.
+   + rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto.
+ - rewrite (div_mod a b) at 1 by order.
+   rewrite mul_add_distr_r.
+   rewrite add_cancel_r.
+   rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
 Qed.
 
 Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c ->
@@ -418,10 +418,10 @@ Proof.
  intros.
  rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))).
  rewrite <- div_mod.
- rewrite div_mul_cancel_l; auto.
- rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
- apply div_mod; order.
- rewrite <- neq_mul_0; intuition; order.
+ - rewrite div_mul_cancel_l; auto.
+   rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
+   apply div_mod; order.
+ - rewrite <- neq_mul_0; intuition; order.
 Qed.
 
 Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c ->
@@ -447,8 +447,8 @@ Proof.
  rewrite add_comm, (mul_comm n), (mul_comm _ b).
  rewrite mul_add_distr_l, mul_assoc.
  intros. rewrite mod_add; auto.
- now rewrite mul_comm.
- apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto.
+ - now rewrite mul_comm.
+ - apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto.
 Qed.
 
 Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -460,8 +460,8 @@ Qed.
 Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a * b) mod n == ((a mod n) * (b mod n)) mod n.
 Proof.
- intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity.
- now destruct (mod_bound_pos b n).
+  intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity.
+  - now destruct (mod_bound_pos b n).
 Qed.
 
 Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -471,8 +471,8 @@ Proof.
  generalize (add_nonneg_nonneg _ _ Ha Hb).
  rewrite (div_mod a n) at 1 2 by order.
  rewrite <- add_assoc, add_comm, mul_comm.
- intros. rewrite mod_add; trivial. reflexivity.
- apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto.
+ intros. rewrite mod_add; trivial. - reflexivity.
+ - apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto.
 Qed.
 
 Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -484,8 +484,8 @@ Qed.
 Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
- intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity.
- now destruct (mod_bound_pos b n).
+  intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity.
+  - now destruct (mod_bound_pos b n).
 Qed.
 
 Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c ->
@@ -494,18 +494,18 @@ Proof.
  intros a b c Ha Hb Hc.
  apply div_unique with (b*((a/b) mod c) + a mod b); trivial.
  (* begin 0<= ... <b*c *)
- destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos.
- split.
- apply add_nonneg_nonneg; auto.
- apply mul_nonneg_nonneg; order.
- apply lt_le_trans with (b*((a/b) mod c) + b).
- rewrite <- add_lt_mono_l; auto.
- rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto.
- (* end 0<= ... < b*c *)
- rewrite (div_mod a b) at 1 by order.
- rewrite add_assoc, add_cancel_r.
- rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
- apply div_mod; order.
+ - destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos.
+   split.
+   + apply add_nonneg_nonneg; auto.
+     apply mul_nonneg_nonneg; order.
+   + apply lt_le_trans with (b*((a/b) mod c) + b).
+     * rewrite <- add_lt_mono_l; auto.
+     * rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto.
+       (* end 0<= ... < b*c *)
+ - rewrite (div_mod a b) at 1 by order.
+   rewrite add_assoc, add_cancel_r.
+   rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
+   apply div_mod; order.
 Qed.
 
 Lemma mod_mul_r : forall a b c, 0<=a -> 0<b -> 0<c ->
@@ -527,10 +527,10 @@ Theorem div_mul_le:
 Proof.
  intros.
  apply div_le_lower_bound; auto.
- apply mul_nonneg_nonneg; auto.
- rewrite mul_assoc, (mul_comm b c), <- mul_assoc.
- apply mul_le_mono_nonneg_l; auto.
- apply mul_div_le; auto.
+ - apply mul_nonneg_nonneg; auto.
+ - rewrite mul_assoc, (mul_comm b c), <- mul_assoc.
+   apply mul_le_mono_nonneg_l; auto.
+   apply mul_div_le; auto.
 Qed.
 
 (** mod is related to divisibility *)
@@ -539,9 +539,9 @@ Lemma mod_divides : forall a b, 0<=a -> 0<b ->
  (a mod b == 0 <-> exists c, a == b*c).
 Proof.
  split.
- intros. exists (a/b). rewrite div_exact; auto.
- intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto.
- rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order.
+ - intros. exists (a/b). rewrite div_exact; auto.
+ - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto.
+   rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order.
 Qed.
 
 End NZDivProp.
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index c38d1aac31..1ac89ce942 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -72,15 +72,15 @@ Lemma eq_mul_1_nonneg : forall n m,
 Proof.
  intros n m Hn H.
  le_elim Hn.
- destruct (lt_ge_cases m 0) as [Hm|Hm].
- generalize (mul_pos_neg n m Hn Hm). order'.
- le_elim Hm.
- apply le_succ_l in Hn. rewrite <- one_succ in 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'.
- rewrite <- Hn, mul_0_l in H. order'.
+ - destruct (lt_ge_cases m 0) as [Hm|Hm].
+   + generalize (mul_pos_neg n m Hn Hm). order'.
+   + le_elim Hm.
+     * apply le_succ_l in Hn. rewrite <- one_succ in 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'.
+ - rewrite <- Hn, mul_0_l in H. order'.
 Qed.
 
 Lemma eq_mul_1_nonneg' : forall n m,
@@ -117,13 +117,13 @@ Lemma divide_antisym_nonneg : forall n m,
 Proof.
  intros n m Hn Hm (q,Hq) (r,Hr).
  le_elim Hn.
- destruct (lt_ge_cases q 0) as [Hq'|Hq'].
- generalize (mul_neg_pos q n Hq' Hn). order.
- rewrite Hq, mul_assoc in Hr. symmetry in Hr.
- apply mul_id_l in Hr; [|order].
- destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial.
- now rewrite H, mul_1_l in Hq.
- rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn.
+ - destruct (lt_ge_cases q 0) as [Hq'|Hq'].
+   + generalize (mul_neg_pos q n Hq' Hn). order.
+   + rewrite Hq, mul_assoc in Hr. symmetry in Hr.
+     apply mul_id_l in Hr; [|order].
+     destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial.
+     now rewrite H, mul_1_l in Hq.
+ - rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn.
 Qed.
 
 Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m).
@@ -140,8 +140,8 @@ Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
  ((p * n | p * m) <-> (n | m)).
 Proof.
  intros n m p Hp. split.
- intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq.
- apply mul_divide_mono_l.
+ - intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq.
+ - apply mul_divide_mono_l.
 Qed.
 
 Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
@@ -179,14 +179,14 @@ Qed.
 Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m.
 Proof.
  intros n m Hm (q,Hq).
- destruct (le_gt_cases n 0) as [Hn|Hn]. order.
- rewrite Hq.
- destruct (lt_ge_cases q 0) as [Hq'|Hq'].
- generalize (mul_neg_pos q n Hq' Hn). order.
- le_elim Hq'.
- rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial.
- now rewrite one_succ, le_succ_l.
- rewrite <- Hq', mul_0_l in Hq. order.
+ destruct (le_gt_cases n 0) as [Hn|Hn]. - order.
+ - rewrite Hq.
+   destruct (lt_ge_cases q 0) as [Hq'|Hq'].
+   + generalize (mul_neg_pos q n Hq' Hn). order.
+   + le_elim Hq'.
+     * rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial.
+       now rewrite one_succ, le_succ_l.
+     * rewrite <- Hq', mul_0_l in Hq. order.
 Qed.
 
 (** Basic properties of gcd *)
@@ -197,28 +197,28 @@ Lemma gcd_unique : forall n m p,
  gcd n m == p.
 Proof.
  intros n m p Hp Hn Hm H.
- apply divide_antisym_nonneg; trivial. apply gcd_nonneg.
- apply H. apply gcd_divide_l. apply gcd_divide_r.
- now apply gcd_greatest.
+ apply divide_antisym_nonneg; trivial. - apply gcd_nonneg.
+ - apply H. + apply gcd_divide_l. + apply gcd_divide_r.
+ - now apply gcd_greatest.
 Qed.
 
 Instance gcd_wd : Proper (eq==>eq==>eq) gcd.
 Proof.
  intros x x' Hx y y' Hy.
  apply gcd_unique.
- apply gcd_nonneg.
- rewrite Hx. apply gcd_divide_l.
- rewrite Hy. apply gcd_divide_r.
- intro. rewrite Hx, Hy. apply gcd_greatest.
+ - apply gcd_nonneg.
+ - rewrite Hx. apply gcd_divide_l.
+ - rewrite Hy. apply gcd_divide_r.
+ - intro. rewrite Hx, Hy. apply gcd_greatest.
 Qed.
 
 Lemma gcd_divide_iff : forall n m p,
   (p | gcd n m) <-> (p | n) /\ (p | m).
 Proof.
- intros. split. split.
- transitivity (gcd n m); trivial using gcd_divide_l.
- transitivity (gcd n m); trivial using gcd_divide_r.
- intros (H,H'). now apply gcd_greatest.
+  intros. split. - split.
+                   + transitivity (gcd n m); trivial using gcd_divide_l.
+                   + transitivity (gcd n m); trivial using gcd_divide_r.
+  - intros (H,H'). now apply gcd_greatest.
 Qed.
 
 Lemma gcd_unique_alt : forall n m p, 0<=p ->
@@ -227,9 +227,9 @@ 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.
- intros. apply H. now split.
+ - apply H. apply divide_refl.
+ - apply H. apply divide_refl.
+ - intros. apply H. now split.
 Qed.
 
 Lemma gcd_comm : forall n m, gcd n m == gcd m n.
@@ -247,8 +247,8 @@ Qed.
 Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n.
 Proof.
  intros. apply gcd_unique; trivial.
- apply divide_0_r.
- apply divide_refl.
+ - apply divide_0_r.
+ - apply divide_refl.
 Qed.
 
 Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n.
@@ -284,24 +284,26 @@ Qed.
 
 Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
 Proof.
- intros. split. split.
- now apply gcd_eq_0_l with m.
- now apply gcd_eq_0_r with n.
- intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg.
+  intros. split.
+  - split.
+    + now apply gcd_eq_0_l with m.
+    + now apply gcd_eq_0_r with n.
+  - intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg.
 Qed.
 
 Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n.
 Proof.
  intros n m Hn. apply gcd_unique_alt; trivial.
- intros q. split. split; trivial. now apply divide_mul_l.
- now destruct 1.
+ intros q. split. - split; trivial. now apply divide_mul_l.
+ - now destruct 1.
 Qed.
 
 Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).
 Proof.
- intros n m Hn. split. intros (q,Hq). rewrite Hq.
- rewrite mul_comm. now apply gcd_mul_diag_l.
- intros EQ. rewrite <- EQ. apply gcd_divide_r.
+  intros n m Hn. split.
+  - intros (q,Hq). rewrite Hq.
+    rewrite mul_comm. now apply gcd_mul_diag_l.
+  - intros EQ. rewrite <- EQ. apply gcd_divide_r.
 Qed.
 
 End NZGcdProp.
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
index 794851a9dd..1951cfc3ef 100644
--- a/theories/Numbers/NatInt/NZLog.v
+++ b/theories/Numbers/NatInt/NZLog.v
@@ -40,10 +40,10 @@ Module Type NZLog2Prop
 Lemma log2_nonneg : forall a, 0 <= log2 a.
 Proof.
  intros a. destruct (le_gt_cases a 0) as [Ha|Ha].
- now rewrite log2_nonpos.
- destruct (log2_spec a Ha) as (_,LT).
- apply lt_succ_r, (pow_gt_1 2). order'.
- rewrite <- le_succ_l, <- one_succ in Ha. order.
+ - now rewrite log2_nonpos.
+ - destruct (log2_spec a Ha) as (_,LT).
+   apply lt_succ_r, (pow_gt_1 2). + order'.
+   + rewrite <- le_succ_l, <- one_succ in Ha. order.
 Qed.
 
 (** A tactic for proving positivity and non-negativity *)
@@ -62,17 +62,17 @@ Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b.
 Proof.
  intros a b Hb (LEb,LTb).
  assert (Ha : 0 < a).
-  apply lt_le_trans with (2^b); trivial.
-  apply pow_pos_nonneg; order'.
- assert (Hc := log2_nonneg a).
- destruct (log2_spec a Ha) as (LEc,LTc).
- assert (log2 a <= b).
-  apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
-  now apply le_le_succ_r.
- assert (b <= log2 a).
-  apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
-  now apply le_le_succ_r.
- order.
+ - apply lt_le_trans with (2^b); trivial.
+   apply pow_pos_nonneg; order'.
+ - assert (Hc := log2_nonneg a).
+   destruct (log2_spec a Ha) as (LEc,LTc).
+   assert (log2 a <= b).
+   + apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
+     now apply le_le_succ_r.
+   + assert (b <= log2 a).
+     * apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
+       now apply le_le_succ_r.
+     * order.
 Qed.
 
 (** Hence log2 is a morphism. *)
@@ -81,9 +81,9 @@ Instance log2_wd : Proper (eq==>eq) log2.
 Proof.
  intros x x' Hx.
  destruct (le_gt_cases x 0).
- rewrite 2 log2_nonpos; trivial. reflexivity. now rewrite <- Hx.
- apply log2_unique. apply log2_nonneg.
- rewrite Hx in *. now apply log2_spec.
+ - rewrite 2 log2_nonpos; trivial. + reflexivity. + now rewrite <- Hx.
+ - apply log2_unique. + apply log2_nonneg.
+   + rewrite Hx in *. now apply log2_spec.
 Qed.
 
 (** An alternate specification *)
@@ -95,24 +95,24 @@ Proof.
  destruct (log2_spec _ Ha) as (LE,LT).
  destruct (le_exists_sub _ _ LE) as (r & Hr & Hr').
  exists r.
- split. now rewrite add_comm.
- split. trivial.
- apply (add_lt_mono_r _ _ (2^log2 a)).
- rewrite <- Hr. generalize LT.
- rewrite pow_succ_r by order_pos.
- rewrite two_succ at 1. now nzsimpl.
+ split. - now rewrite add_comm.
+ - split. + trivial.
+   + apply (add_lt_mono_r _ _ (2^log2 a)).
+     rewrite <- Hr. generalize LT.
+     rewrite pow_succ_r by order_pos.
+     rewrite two_succ at 1. now nzsimpl.
 Qed.
 
 Lemma log2_unique' : forall a b c, 0<=b -> 0<=c<2^b ->
  a == 2^b + c -> log2 a == b.
 Proof.
  intros a b c Hb (Hc,H) EQ.
- apply log2_unique. trivial.
- rewrite EQ.
- split.
- rewrite <- add_0_r at 1. now apply add_le_mono_l.
- rewrite pow_succ_r by order.
- rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l.
+ apply log2_unique. - trivial.
+ - rewrite EQ.
+   split.
+   + rewrite <- add_0_r at 1. now apply add_le_mono_l.
+   + rewrite pow_succ_r by order.
+     rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l.
 Qed.
 
 (** log2 is exact on powers of 2 *)
@@ -121,7 +121,7 @@ Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a.
 Proof.
  intros a Ha.
  apply log2_unique' with 0; trivial.
- split; order_pos. now nzsimpl.
+ - split; order_pos. - now nzsimpl.
 Qed.
 
 (** log2 and predecessors of powers of 2 *)
@@ -131,12 +131,12 @@ Proof.
  intros a Ha.
  assert (Ha' : S (P a) == a) by (now rewrite lt_succ_pred with 0).
  apply log2_unique.
- apply lt_succ_r; order.
- rewrite <-le_succ_l, <-lt_succ_r, Ha'.
- rewrite lt_succ_pred with 0.
- split; try easy. apply pow_lt_mono_r_iff; try order'.
-  rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r.
- apply pow_pos_nonneg; order'.
+ - apply lt_succ_r; order.
+ - rewrite <-le_succ_l, <-lt_succ_r, Ha'.
+   rewrite lt_succ_pred with 0.
+   + split; try easy. apply pow_lt_mono_r_iff; try order'.
+     rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r.
+   + apply pow_pos_nonneg; order'.
 Qed.
 
 (** log2 and basic constants *)
@@ -167,11 +167,11 @@ Qed.
 Lemma log2_null : forall a, log2 a == 0 <-> a <= 1.
 Proof.
  intros a. split; intros H.
- destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
- generalize (log2_pos a Ha); order.
- le_elim H.
- apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ.
- rewrite H. apply log2_1.
+ - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
+   generalize (log2_pos a Ha); order.
+ - le_elim H.
+   + apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ.
+   + rewrite H. apply log2_1.
 Qed.
 
 (** log2 is a monotone function (but not a strict one) *)
@@ -180,11 +180,11 @@ Lemma log2_le_mono : forall a b, a<=b -> log2 a <= log2 b.
 Proof.
  intros a b H.
  destruct (le_gt_cases a 0) as [Ha|Ha].
- rewrite log2_nonpos; order_pos.
- assert (Hb : 0 < b) by order.
- destruct (log2_spec a Ha) as (LEa,_).
- destruct (log2_spec b Hb) as (_,LTb).
- apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos.
+ - rewrite log2_nonpos; order_pos.
+ - assert (Hb : 0 < b) by order.
+   destruct (log2_spec a Ha) as (LEa,_).
+   destruct (log2_spec b Hb) as (_,LTb).
+   apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos.
 Qed.
 
 (** No reverse result for <=, consider for instance log2 3 <= log2 2 *)
@@ -193,13 +193,13 @@ Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b.
 Proof.
  intros a b H.
  destruct (le_gt_cases b 0) as [Hb|Hb].
-  rewrite (log2_nonpos b) in H; trivial.
-  generalize (log2_nonneg a); order.
- destruct (le_gt_cases a 0) as [Ha|Ha]. order.
- destruct (log2_spec a Ha) as (_,LTa).
- destruct (log2_spec b Hb) as (LEb,_).
- apply le_succ_l in H.
- apply (pow_le_mono_r_iff 2) in H; order_pos.
+ - rewrite (log2_nonpos b) in H; trivial.
+   generalize (log2_nonneg a); order.
+ - destruct (le_gt_cases a 0) as [Ha|Ha]. + order.
+   + destruct (log2_spec a Ha) as (_,LTa).
+     destruct (log2_spec b Hb) as (LEb,_).
+     apply le_succ_l in H.
+     apply (pow_le_mono_r_iff 2) in H; order_pos.
 Qed.
 
 (** When left side is a power of 2, we have an equivalence for <= *)
@@ -208,12 +208,12 @@ Lemma log2_le_pow2 : forall a b, 0<a -> (2^b<=a <-> b <= log2 a).
 Proof.
  intros a b Ha.
  split; intros H.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- generalize (log2_nonneg a); order.
- rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono.
- transitivity (2^(log2 a)).
- apply pow_le_mono_r; order'.
- now destruct (log2_spec a Ha).
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + generalize (log2_nonneg a); order.
+   + rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono.
+ - transitivity (2^(log2 a)).
+   + apply pow_le_mono_r; order'.
+   + now destruct (log2_spec a Ha).
 Qed.
 
 (** When right side is a square, we have an equivalence for < *)
@@ -222,15 +222,15 @@ Lemma log2_lt_pow2 : forall a b, 0<a -> (a<2^b <-> log2 a < b).
 Proof.
  intros a b Ha.
  split; intros H.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- rewrite pow_neg_r in H; order.
- apply (pow_lt_mono_r_iff 2); try order_pos.
- apply le_lt_trans with a; trivial.
- now destruct (log2_spec a Ha).
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- generalize (log2_nonneg a); order.
- apply log2_lt_cancel; try order.
- now rewrite log2_pow2.
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + rewrite pow_neg_r in H; order.
+   + apply (pow_lt_mono_r_iff 2); try order_pos.
+     apply le_lt_trans with a; trivial.
+     now destruct (log2_spec a Ha).
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + generalize (log2_nonneg a); order.
+   + apply log2_lt_cancel; try order.
+     now rewrite log2_pow2.
 Qed.
 
 (** Comparing log2 and identity *)
@@ -240,16 +240,16 @@ Proof.
  intros a Ha.
  apply (pow_lt_mono_r_iff 2); try order_pos.
  apply le_lt_trans with a.
- now destruct (log2_spec a Ha).
- apply pow_gt_lin_r; order'.
+ - now destruct (log2_spec a Ha).
+ - apply pow_gt_lin_r; order'.
 Qed.
 
 Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a.
 Proof.
  intros a Ha.
  le_elim Ha.
- now apply lt_le_incl, log2_lt_lin.
- rewrite <- Ha, log2_nonpos; order.
+ - now apply lt_le_incl, log2_lt_lin.
+ - rewrite <- Ha, log2_nonpos; order.
 Qed.
 
 (** Log2 and multiplication. *)
@@ -271,14 +271,14 @@ Lemma log2_mul_above : forall a b, 0<=a -> 0<=b ->
 Proof.
  intros a b Ha 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.
- rewrite pow_add_r by order_pos.
- apply mul_lt_mono_nonneg; try order; now apply log2_spec.
- rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos.
- rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos.
+ - le_elim Hb.
+   + apply lt_succ_r.
+     rewrite add_1_r, <- add_succ_r, <- add_succ_l.
+     apply log2_lt_pow2; try order_pos.
+     rewrite pow_add_r by order_pos.
+     apply mul_lt_mono_nonneg; try order; now apply log2_spec.
+   + rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos.
+ - rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos.
 Qed.
 
 (** And we can't find better approximations in general.
@@ -293,10 +293,10 @@ Lemma log2_mul_pow2 : forall a b, 0<a -> 0<=b -> log2 (a*2^b) == b + log2 a.
 Proof.
  intros a b Ha Hb.
  apply log2_unique; try order_pos. split.
- rewrite pow_add_r, mul_comm; try order_pos.
- apply mul_le_mono_nonneg_r. order_pos. now apply log2_spec.
- rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos.
- apply mul_lt_mono_pos_l. order_pos. now apply log2_spec.
+ - rewrite pow_add_r, mul_comm; try order_pos.
+   apply mul_le_mono_nonneg_r. + order_pos. + now apply log2_spec.
+ - rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos.
+   apply mul_lt_mono_pos_l. + order_pos. + now apply log2_spec.
 Qed.
 
 Lemma log2_double : forall a, 0<a -> log2 (2*a) == S (log2 a).
@@ -323,13 +323,13 @@ Lemma log2_succ_le : forall a, log2 (S a) <= S (log2 a).
 Proof.
  intros a.
  destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]].
- apply (pow_le_mono_r_iff 2); try order_pos.
- transitivity (S a).
- apply log2_spec.
- apply lt_succ_r; order.
- now apply le_succ_l, log2_spec.
- rewrite <- EQ, <- one_succ, log2_1; order_pos.
- rewrite 2 log2_nonpos. order_pos. order'. now rewrite le_succ_l.
+ - apply (pow_le_mono_r_iff 2); try order_pos.
+   transitivity (S a).
+   + apply log2_spec.
+     apply lt_succ_r; order.
+   + now apply le_succ_l, log2_spec.
+ - rewrite <- EQ, <- one_succ, log2_1; order_pos.
+ - rewrite 2 log2_nonpos. + order_pos. + order'. + now rewrite le_succ_l.
 Qed.
 
 Lemma log2_succ_or : forall a,
@@ -337,8 +337,8 @@ Lemma log2_succ_or : forall a,
 Proof.
  intros.
  destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H].
- right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order.
- left. apply le_succ_l in H. generalize (log2_succ_le a); order.
+ - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order.
+ - left. apply le_succ_l in H. generalize (log2_succ_le a); order.
 Qed.
 
 Lemma log2_eq_succ_is_pow2 : forall a,
@@ -346,27 +346,27 @@ Lemma log2_eq_succ_is_pow2 : forall a,
 Proof.
  intros a H.
  destruct (le_gt_cases a 0) as [Ha|Ha].
- rewrite 2 (proj2 (log2_null _)) in H. generalize (lt_succ_diag_r 0); order.
- order'. apply le_succ_l. order'.
- assert (Ha' : 0 < S a) by (apply lt_succ_r; order).
- exists (log2 (S a)).
- generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)).
- rewrite <- le_succ_l, <- H. order.
+ - rewrite 2 (proj2 (log2_null _)) in H. + generalize (lt_succ_diag_r 0); order.
+   + order'. + apply le_succ_l. order'.
+ - assert (Ha' : 0 < S a) by (apply lt_succ_r; order).
+   exists (log2 (S a)).
+   generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)).
+   rewrite <- le_succ_l, <- H. order.
 Qed.
 
 Lemma log2_eq_succ_iff_pow2 : forall a, 0<a ->
  (log2 (S a) == S (log2 a) <-> exists b, S a == 2^b).
 Proof.
  intros a Ha.
- split. apply log2_eq_succ_is_pow2.
- intros (b,Hb).
- assert (Hb' : 0 < b).
-  apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono.
- rewrite Hb, log2_pow2; try order'.
- setoid_replace a with (P (2^b)). rewrite log2_pred_pow2; trivial.
- symmetry; now apply lt_succ_pred with 0.
- apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0.
-  rewrite <- Hb, lt_succ_r; order.
+ split. - apply log2_eq_succ_is_pow2.
+ - intros (b,Hb).
+   assert (Hb' : 0 < b).
+   + apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono.
+   + rewrite Hb, log2_pow2; try order'.
+     setoid_replace a with (P (2^b)). * rewrite log2_pred_pow2; trivial.
+                                        symmetry; now apply lt_succ_pred with 0.
+     * apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0.
+       rewrite <- Hb, lt_succ_r; order.
 Qed.
 
 Lemma log2_succ_double : forall a, 0<a -> log2 (2*a+1) == S (log2 a).
@@ -376,18 +376,18 @@ Proof.
  destruct (log2_succ_or (2*a)) as [H|H]; [exfalso|now rewrite H, log2_double].
  apply log2_eq_succ_is_pow2 in H. destruct H as (b,H).
  destruct (lt_trichotomy b 0) as [LT|[EQ|LT]].
- rewrite pow_neg_r in H; trivial.
- apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'.
- rewrite <- one_succ in Ha. order'.
- rewrite EQ, pow_0_r in H.
- apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'.
- rewrite <- one_succ in Ha. order'.
- assert (EQ:=lt_succ_pred 0 b LT).
- rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ].
- destruct (lt_ge_cases a (2^(P b))) as [LT'|LE'].
- generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order.
- rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'.
- rewrite <- H in LE'. apply le_succ_l in LE'. order.
+ - rewrite pow_neg_r in H; trivial.
+   apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'.
+   rewrite <- one_succ in Ha. order'.
+ - rewrite EQ, pow_0_r in H.
+   apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'.
+   rewrite <- one_succ in Ha. order'.
+ - assert (EQ:=lt_succ_pred 0 b LT).
+   rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ].
+   destruct (lt_ge_cases a (2^(P b))) as [LT'|LE'].
+   + generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order.
+   + rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'.
+     rewrite <- H in LE'. apply le_succ_l in LE'. order.
 Qed.
 
 (** Log2 and addition *)
@@ -396,25 +396,28 @@ Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b.
 Proof.
  intros a b Ha Hb.
  destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|].
- rewrite one_succ, lt_succ_r in Ha'.
- rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono.
- rewrite <- (add_0_l b) at 2. now apply add_le_mono.
- destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
- rewrite one_succ, lt_succ_r in Hb'.
- rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono.
- rewrite <- (add_0_r a) at 2. now apply add_le_mono.
- clear Ha Hb.
- apply lt_succ_r.
- apply log2_lt_pow2; try order_pos.
- rewrite pow_succ_r by order_pos.
- rewrite two_succ, one_succ at 1. nzsimpl.
- apply add_lt_mono.
- apply lt_le_trans with (2^(S (log2 a))). apply log2_spec; order'.
- apply pow_le_mono_r. order'. rewrite <- add_1_r. apply add_le_mono_l.
-  rewrite one_succ; now apply le_succ_l, log2_pos.
- apply lt_le_trans with (2^(S (log2 b))). apply log2_spec; order'.
- apply pow_le_mono_r. order'. rewrite <- add_1_l. apply add_le_mono_r.
-  rewrite one_succ; now apply le_succ_l, log2_pos.
+ - rewrite one_succ, lt_succ_r in Ha'.
+   rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono.
+   rewrite <- (add_0_l b) at 2. now apply add_le_mono.
+ - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
+   + rewrite one_succ, lt_succ_r in Hb'.
+     rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono.
+     rewrite <- (add_0_r a) at 2. now apply add_le_mono.
+   + clear Ha Hb.
+     apply lt_succ_r.
+     apply log2_lt_pow2; try order_pos.
+     rewrite pow_succ_r by order_pos.
+     rewrite two_succ, one_succ at 1. nzsimpl.
+     apply add_lt_mono.
+     * apply lt_le_trans with (2^(S (log2 a))). -- apply log2_spec; order'.
+       -- apply pow_le_mono_r. ++ order'.
+          ++ rewrite <- add_1_r. apply add_le_mono_l.
+             rewrite one_succ; now apply le_succ_l, log2_pos.
+     * apply lt_le_trans with (2^(S (log2 b))).
+       -- apply log2_spec; order'.
+       -- apply pow_le_mono_r. ++ order'.
+          ++ rewrite <- add_1_l. apply add_le_mono_r.
+             rewrite one_succ; now apply le_succ_l, log2_pos.
 Qed.
 
 (** The sum of two log2 is less than twice the log2 of the sum.
@@ -430,17 +433,17 @@ Lemma add_log2_lt : forall a b, 0<a -> 0<b ->
 Proof.
  intros a b Ha Hb. nzsimpl'.
  assert (H : log2 a <= log2 (a+b)).
-  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.
- 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.
- 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.
+ - 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.
+   + 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.
+       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.
 Qed.
 
 End NZLog2Prop.
@@ -493,9 +496,9 @@ Qed.
 Instance log2_up_wd : Proper (eq==>eq) log2_up.
 Proof.
  assert (Proper (eq==>eq==>Logic.eq) compare).
-  repeat red; intros; do 2 case compare_spec; trivial; order.
- intros a a' Ha. unfold log2_up. rewrite Ha at 1.
- case compare; now rewrite ?Ha.
+ - repeat red; intros; do 2 case compare_spec; trivial; order.
+ - intros a a' Ha. unfold log2_up. rewrite Ha at 1.
+   case compare; now rewrite ?Ha.
 Qed.
 
 (** [log2_up] is always non-negative *)
@@ -512,22 +515,23 @@ Lemma log2_up_unique : forall a b, 0<b -> 2^(P b)<a<=2^b -> log2_up a == b.
 Proof.
  intros a b Hb (LEb,LTb).
  assert (Ha : 1 < a).
-  apply le_lt_trans with (2^(P b)); trivial.
-  rewrite one_succ. apply le_succ_l.
-  apply pow_pos_nonneg. order'. apply lt_succ_r.
-  now rewrite (lt_succ_pred 0 b Hb).
- assert (Hc := log2_up_nonneg a).
- destruct (log2_up_spec a Ha) as (LTc,LEc).
- assert (b <= log2_up a).
-  apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb).
-  rewrite <- succ_lt_mono.
-  apply (pow_lt_mono_r_iff 2); try order'.
- assert (Hc' : 0 < log2_up a) by order.
- assert (log2_up a <= b).
-  apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc').
-  rewrite <- succ_lt_mono.
-  apply (pow_lt_mono_r_iff 2); try order'.
- order.
+ - apply le_lt_trans with (2^(P b)); trivial.
+   rewrite one_succ. apply le_succ_l.
+   apply pow_pos_nonneg. + order'.
+   + apply lt_succ_r.
+     now rewrite (lt_succ_pred 0 b Hb).
+ - assert (Hc := log2_up_nonneg a).
+   destruct (log2_up_spec a Ha) as (LTc,LEc).
+   assert (b <= log2_up a).
+   + apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb).
+     rewrite <- succ_lt_mono.
+     apply (pow_lt_mono_r_iff 2); try order'.
+   + assert (Hc' : 0 < log2_up a) by order.
+     assert (log2_up a <= b).
+     * apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc').
+       rewrite <- succ_lt_mono.
+       apply (pow_lt_mono_r_iff 2); try order'.
+     * order.
 Qed.
 
 (** [log2_up] is exact on powers of 2 *)
@@ -536,12 +540,12 @@ Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a.
 Proof.
  intros a Ha.
  le_elim Ha.
- apply log2_up_unique; trivial.
- split; try order.
- apply pow_lt_mono_r; try order'.
- rewrite <- (lt_succ_pred 0 a Ha) at 2.
- now apply lt_succ_r.
- now rewrite <- Ha, pow_0_r, log2_up_eqn0.
+ - apply log2_up_unique; trivial.
+   split; try order.
+   apply pow_lt_mono_r; try order'.
+   rewrite <- (lt_succ_pred 0 a Ha) at 2.
+   now apply lt_succ_r.
+ - now rewrite <- Ha, pow_0_r, log2_up_eqn0.
 Qed.
 
 (** [log2_up] and successors of powers of 2 *)
@@ -570,9 +574,9 @@ Qed.
 Lemma le_log2_log2_up : forall a, log2 a <= log2_up a.
 Proof.
  intros a. unfold log2_up. case compare_spec; intros H.
- rewrite <- H, log2_1. order.
- rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le.
- rewrite log2_nonpos. order. now rewrite <-lt_succ_r, <-one_succ.
+ - rewrite <- H, log2_1. order.
+ - rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le.
+ - rewrite log2_nonpos. + order. + now rewrite <-lt_succ_r, <-one_succ.
 Qed.
 
 Lemma le_log2_up_succ_log2 : forall a, log2_up a <= S (log2 a).
@@ -586,23 +590,24 @@ Lemma log2_log2_up_spec : forall a, 0<a ->
  2^log2 a <= a <= 2^log2_up a.
 Proof.
  intros a H. split.
- now apply log2_spec.
- 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.
+ - now apply log2_spec.
+ - 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.
 
 Lemma log2_log2_up_exact :
  forall a, 0<a -> (log2 a == log2_up a <-> exists b, a == 2^b).
 Proof.
  intros a Ha.
- split. intros. exists (log2 a).
-  generalize (log2_log2_up_spec a Ha). rewrite <-H.
-  destruct 1; order.
- intros (b,Hb). rewrite Hb.
- destruct (le_gt_cases 0 b).
- now rewrite log2_pow2, log2_up_pow2.
- rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos.
+ split.
+ - intros. exists (log2 a).
+   generalize (log2_log2_up_spec a Ha). rewrite <-H.
+   destruct 1; order.
+ - intros (b,Hb). rewrite Hb.
+   destruct (le_gt_cases 0 b).
+   + now rewrite log2_pow2, log2_up_pow2.
+   + rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos.
 Qed.
 
 (** [log2_up] n is strictly positive for 1<n *)
@@ -617,9 +622,9 @@ Qed.
 Lemma log2_up_null : forall a, log2_up a == 0 <-> a <= 1.
 Proof.
  intros a. split; intros H.
- destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
- generalize (log2_up_pos a Ha); order.
- now apply log2_up_eqn0.
+ - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
+   generalize (log2_up_pos a Ha); order.
+ - now apply log2_up_eqn0.
 Qed.
 
 (** [log2_up] is a monotone function (but not a strict one) *)
@@ -628,10 +633,10 @@ Lemma log2_up_le_mono : forall a b, a<=b -> log2_up a <= log2_up b.
 Proof.
  intros a b H.
  destruct (le_gt_cases a 1) as [Ha|Ha].
- rewrite log2_up_eqn0; trivial. apply log2_up_nonneg.
- rewrite 2 log2_up_eqn; try order.
- rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono.
- rewrite 2 lt_succ_pred with 1; order.
+ - rewrite log2_up_eqn0; trivial. apply log2_up_nonneg.
+ - rewrite 2 log2_up_eqn; try order.
+   rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono.
+   rewrite 2 lt_succ_pred with 1; order.
 Qed.
 
 (** No reverse result for <=, consider for instance log2_up 4 <= log2_up 3 *)
@@ -640,12 +645,12 @@ Lemma log2_up_lt_cancel : forall a b, log2_up a < log2_up b -> a < b.
 Proof.
  intros a b H.
  destruct (le_gt_cases b 1) as [Hb|Hb].
-  rewrite (log2_up_eqn0 b) in H; trivial.
-  generalize (log2_up_nonneg a); order.
- destruct (le_gt_cases a 1) as [Ha|Ha]. order.
- rewrite 2 log2_up_eqn in H; try order.
- rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H.
- rewrite 2 lt_succ_pred with 1 in H; order.
+ - rewrite (log2_up_eqn0 b) in H; trivial.
+   generalize (log2_up_nonneg a); order.
+ - destruct (le_gt_cases a 1) as [Ha|Ha]. + order.
+   + rewrite 2 log2_up_eqn in H; try order.
+     rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H.
+     rewrite 2 lt_succ_pred with 1 in H; order.
 Qed.
 
 (** When left side is a power of 2, we have an equivalence for < *)
@@ -654,16 +659,16 @@ Lemma log2_up_lt_pow2 : forall a b, 0<a -> (2^b<a <-> b < log2_up a).
 Proof.
  intros a b Ha.
  split; intros H.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- generalize (log2_up_nonneg a); order.
- apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg.
- apply lt_le_trans with a; trivial.
- apply (log2_up_spec a).
- apply le_lt_trans with (2^b); trivial.
- rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- now rewrite pow_neg_r.
- rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel.
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + generalize (log2_up_nonneg a); order.
+   + apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg.
+     * apply lt_le_trans with a; trivial.
+       apply (log2_up_spec a).
+       apply le_lt_trans with (2^b); trivial.
+       rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'.
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + now rewrite pow_neg_r.
+   + rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel.
 Qed.
 
 (** When right side is a square, we have an equivalence for <= *)
@@ -672,12 +677,12 @@ Lemma log2_up_le_pow2 : forall a b, 0<a -> (a<=2^b <-> log2_up a <= b).
 Proof.
  intros a b Ha.
  split; intros H.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- rewrite pow_neg_r in H; order.
- rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono.
- transitivity (2^(log2_up a)).
- now apply log2_log2_up_spec.
- apply pow_le_mono_r; order'.
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + rewrite pow_neg_r in H; order.
+   + rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono.
+ - transitivity (2^(log2_up a)).
+   + now apply log2_log2_up_spec.
+   + apply pow_le_mono_r; order'.
 Qed.
 
 (** Comparing [log2_up] and identity *)
@@ -688,15 +693,15 @@ Proof.
  assert (H : S (P a) == a) by (now apply lt_succ_pred with 0).
  rewrite <- H at 2. apply lt_succ_r. apply log2_up_le_pow2; trivial.
  rewrite <- H at 1. apply le_succ_l.
- apply pow_gt_lin_r. order'. apply lt_succ_r; order.
+ apply pow_gt_lin_r. - order'. - apply lt_succ_r; order.
 Qed.
 
 Lemma log2_up_le_lin : forall a, 0<=a -> log2_up a <= a.
 Proof.
  intros a Ha.
  le_elim Ha.
- now apply lt_le_incl, log2_up_lt_lin.
- rewrite <- Ha, log2_up_nonpos; order.
+ - now apply lt_le_incl, log2_up_lt_lin.
+ - rewrite <- Ha, log2_up_nonpos; order.
 Qed.
 
 (** [log2_up] and multiplication. *)
@@ -711,12 +716,12 @@ Proof.
  assert (Ha':=log2_up_nonneg a).
  assert (Hb':=log2_up_nonneg b).
  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'.
- rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos.
- rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos.
+ - 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'.
+   + rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos.
+ - rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos.
 Qed.
 
 Lemma log2_up_mul_below : forall a b, 0<a -> 0<b ->
@@ -724,21 +729,21 @@ Lemma log2_up_mul_below : forall a b, 0<a -> 0<b ->
 Proof.
  intros a b Ha 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.
- rewrite <- (lt_succ_pred 0 (log2_up b)); trivial.
- nzsimpl. rewrite <- succ_le_mono, le_succ_l.
- apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg.
- rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial).
- apply lt_le_trans with (a*b).
- apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec.
- apply log2_up_spec.
- setoid_replace 1 with (1*1) by now nzsimpl.
- apply mul_lt_mono_nonneg; order'.
- rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r.
- rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r.
+ - 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.
+     rewrite <- (lt_succ_pred 0 (log2_up b)); trivial.
+     nzsimpl. rewrite <- succ_le_mono, le_succ_l.
+     apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg.
+     * rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial).
+       apply lt_le_trans with (a*b).
+       -- apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec.
+       -- apply log2_up_spec.
+          setoid_replace 1 with (1*1) by now nzsimpl.
+          apply mul_lt_mono_nonneg; order'.
+   + rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r.
+ - rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r.
 Qed.
 
 (** And we can't find better approximations in general.
@@ -754,16 +759,16 @@ Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b ->
 Proof.
  intros a b Ha Hb.
  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)).
- rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial.
- apply mul_lt_mono_pos_r. order_pos. now apply log2_up_spec.
- rewrite <- lt_succ_r, EQ. now apply log2_up_pos.
- rewrite pow_add_r, mul_comm; trivial.
- apply mul_le_mono_nonneg_l. order_pos. now apply log2_up_spec.
- apply log2_up_nonneg.
- now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2.
+ - 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)).
+       rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial.
+       -- apply mul_lt_mono_pos_r. ++ order_pos. ++ now apply log2_up_spec.
+       -- rewrite <- lt_succ_r, EQ. now apply log2_up_pos.
+     * rewrite pow_add_r, mul_comm; trivial.
+       -- apply mul_le_mono_nonneg_l. ++ order_pos. ++ now apply log2_up_spec.
+       -- apply log2_up_nonneg.
+ - now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2.
 Qed.
 
 Lemma log2_up_double : forall a, 0<a -> log2_up (2*a) == S (log2_up a).
@@ -790,12 +795,12 @@ Lemma log2_up_succ_le : forall a, log2_up (S a) <= S (log2_up a).
 Proof.
  intros a.
  destruct (lt_trichotomy 1 a) as [LT|[EQ|LT]].
- rewrite 2 log2_up_eqn; trivial.
- rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1.
- apply log2_succ_le.
- apply lt_succ_r; order.
- rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'.
- rewrite 2 log2_up_eqn0. order_pos. order'. now rewrite le_succ_l.
+ - rewrite 2 log2_up_eqn; trivial.
+   + rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1.
+     apply log2_succ_le.
+   + apply lt_succ_r; order.
+ - rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'.
+ - rewrite 2 log2_up_eqn0. + order_pos. + order'. + now rewrite le_succ_l.
 Qed.
 
 Lemma log2_up_succ_or : forall a,
@@ -803,8 +808,8 @@ Lemma log2_up_succ_or : forall a,
 Proof.
  intros.
  destruct (le_gt_cases (log2_up (S a)) (log2_up a)).
- right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order.
- left. apply le_succ_l in H. generalize (log2_up_succ_le a); order.
+ - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order.
+ - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order.
 Qed.
 
 Lemma log2_up_eq_succ_is_pow2 : forall a,
@@ -812,33 +817,33 @@ Lemma log2_up_eq_succ_is_pow2 : forall a,
 Proof.
  intros a H.
  destruct (le_gt_cases a 0) as [Ha|Ha].
- rewrite 2 (proj2 (log2_up_null _)) in H. generalize (lt_succ_diag_r 0); order.
- order'. apply le_succ_l. order'.
- assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono).
- exists (log2_up a).
- generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)).
- rewrite H, pred_succ, lt_succ_r. order.
+ - rewrite 2 (proj2 (log2_up_null _)) in H. + generalize (lt_succ_diag_r 0); order.
+   + order'. + apply le_succ_l. order'.
+ - assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono).
+   exists (log2_up a).
+   generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)).
+   rewrite H, pred_succ, lt_succ_r. order.
 Qed.
 
 Lemma log2_up_eq_succ_iff_pow2 : forall a, 0<a ->
  (log2_up (S a) == S (log2_up a) <-> exists b, a == 2^b).
 Proof.
  intros a Ha.
- split. apply log2_up_eq_succ_is_pow2.
- intros (b,Hb).
- destruct (lt_ge_cases b 0) as [Hb'|Hb'].
-  rewrite pow_neg_r in Hb; order.
- rewrite Hb, log2_up_pow2; try order'.
- now rewrite log2_up_succ_pow2.
+ split. - apply log2_up_eq_succ_is_pow2.
+ - intros (b,Hb).
+   destruct (lt_ge_cases b 0) as [Hb'|Hb'].
+   + rewrite pow_neg_r in Hb; order.
+   + rewrite Hb, log2_up_pow2; try order'.
+     now rewrite log2_up_succ_pow2.
 Qed.
 
 Lemma log2_up_succ_double : forall a, 0<a ->
  log2_up (2*a+1) == 2 + log2 a.
 Proof.
  intros a Ha.
- rewrite log2_up_eqn. rewrite add_1_r, pred_succ, log2_double; now nzsimpl'.
- apply le_lt_trans with (0+1). now nzsimpl'.
- apply add_lt_mono_r. order_pos.
+ rewrite log2_up_eqn. - rewrite add_1_r, pred_succ, log2_double; now nzsimpl'.
+ - apply le_lt_trans with (0+1). + now nzsimpl'.
+   + apply add_lt_mono_r. order_pos.
 Qed.
 
 (** [log2_up] and addition *)
@@ -848,17 +853,17 @@ Lemma log2_up_add_le : forall a b, a~=1 -> b~=1 ->
 Proof.
  intros a b Ha Hb.
  destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|].
- rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono.
- rewrite one_succ, lt_succ_r in Ha'.
- rewrite <- (add_0_l b) at 2. now apply add_le_mono.
- destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
- rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono.
- rewrite one_succ, lt_succ_r in Hb'.
- rewrite <- (add_0_r a) at 2. now apply add_le_mono.
- clear Ha Hb.
- transitivity (log2_up (a*b)).
- now apply log2_up_le_mono, add_le_mul.
- apply log2_up_mul_above; order'.
+ - rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono.
+   rewrite one_succ, lt_succ_r in Ha'.
+   rewrite <- (add_0_l b) at 2. now apply add_le_mono.
+ - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
+   + rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono.
+     rewrite one_succ, lt_succ_r in Hb'.
+     rewrite <- (add_0_r a) at 2. now apply add_le_mono.
+   + clear Ha Hb.
+     transitivity (log2_up (a*b)).
+     * now apply log2_up_le_mono, add_le_mul.
+     * apply log2_up_mul_above; order'.
 Qed.
 
 (** The sum of two [log2_up] is less than twice the [log2_up] of the sum.
@@ -874,17 +879,17 @@ Lemma add_log2_up_lt : forall a b, 0<a -> 0<b ->
 Proof.
  intros a b Ha Hb. nzsimpl'.
  assert (H : log2_up a <= log2_up (a+b)).
-  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.
- 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.
- 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.
+ - 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.
+   + 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.
+       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.
 Qed.
 
 End NZLog2UpProp.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 44cbc51712..1492188452 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -22,24 +22,27 @@ Qed.
 
 Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
 Proof.
-intros n m; nzinduct n. now nzsimpl.
-intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc.
-now rewrite add_cancel_r.
+  intros n m; nzinduct n.
+  - now nzsimpl.
+  - intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc.
+    now rewrite add_cancel_r.
 Qed.
 
 Hint Rewrite mul_0_r mul_succ_r : nz.
 
 Theorem mul_comm : forall n m, n * m == m * n.
 Proof.
-intros n m; nzinduct n. now nzsimpl.
-intro. nzsimpl. now rewrite add_cancel_r.
+  intros n m; nzinduct n.
+  - now nzsimpl.
+  - intro. nzsimpl. now rewrite add_cancel_r.
 Qed.
 
 Theorem mul_add_distr_r : forall n m p, (n + m) * p == n * p + m * p.
 Proof.
-intros n m p; nzinduct n. now nzsimpl.
-intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc.
-now rewrite add_cancel_r.
+  intros n m p; nzinduct n.
+  - now nzsimpl.
+  - intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc.
+    now rewrite add_cancel_r.
 Qed.
 
 Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p.
@@ -51,9 +54,9 @@ Qed.
 
 Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p.
 Proof.
-intros n m p; nzinduct n. now nzsimpl.
-intro n. nzsimpl. rewrite mul_add_distr_r.
-now rewrite add_cancel_r.
+  intros n m p; nzinduct n. - now nzsimpl.
+  - intro n. nzsimpl. rewrite mul_add_distr_r.
+    now rewrite add_cancel_r.
 Qed.
 
 Theorem mul_1_l : forall n, 1 * n == n.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 292f0837c0..dc4167e96f 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -26,16 +26,16 @@ Qed.
 
 Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m).
 Proof.
-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.
+  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).
@@ -47,19 +47,20 @@ Qed.
 Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).
 Proof.
 nzord_induct p.
-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.
+- 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).
@@ -71,17 +72,17 @@ 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.
-apply eq_le_incl; now rewrite H2.
-apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_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.
 
 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.
-apply eq_le_incl; now rewrite H2.
-apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_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.
 
 Theorem mul_le_mono_nonneg_r : forall n m p, 0 <= p -> n <= m -> n * p <= m * p.
@@ -101,10 +102,10 @@ Proof.
 intros n m p Hp; split; intro H; [|now f_equiv].
 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.
+- 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).
@@ -155,8 +156,8 @@ Theorem mul_lt_mono_nonneg :
 Proof.
 intros n m p q H1 H2 H3 H4.
 apply le_lt_trans with (m * p).
-apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
-apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n].
+- apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
+- apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n].
 Qed.
 
 (* There are still many variants of the theorem above. One can assume 0 < n
@@ -167,10 +168,10 @@ Theorem mul_le_mono_nonneg :
 Proof.
 intros n m p q H1 H2 H3 H4.
 le_elim H2; le_elim H4.
-apply lt_le_incl; now apply mul_lt_mono_nonneg.
-rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
-rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl].
-rewrite H2; rewrite H4; now apply eq_le_incl.
+- apply lt_le_incl; now apply mul_lt_mono_nonneg.
+- rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
+- rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl].
+- rewrite H2; rewrite H4; now apply eq_le_incl.
 Qed.
 
 Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m.
@@ -225,29 +226,29 @@ 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.
-rewrite mul_1_l in H1. now apply lt_1_l with m.
-assumption.
+- rewrite mul_1_l in H1. now apply lt_1_l with m.
+- assumption.
 Qed.
 
 Theorem eq_mul_0 : forall n m, n * m == 0 <-> n == 0 \/ m == 0.
 Proof.
 intros n m; split.
-intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
-destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
-try (now right); try (now left).
-exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |].
-exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |].
-exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |].
-exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |].
-intros [H | H]. now rewrite H, mul_0_l. now rewrite H, mul_0_r.
+- intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
+    destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
+    try (now right); try (now left).
+  + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |].
+  + exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |].
+  + exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |].
+  + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |].
+- intros [H | H]. + now rewrite H, mul_0_l. + now rewrite H, mul_0_r.
 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.
-split; intro H1; rewrite H1 in H;
-(rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H.
+- 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.
 
 Theorem eq_square_0 : forall n, n * n == 0 <-> n == 0.
@@ -258,13 +259,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].
-assumption. false_hyp H1 H2.
+- 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].
-false_hyp H1 H2. assumption.
+- false_hyp H1 H2. - assumption.
 Qed.
 
 (** Some alternative names: *)
@@ -276,16 +277,16 @@ Definition mul_eq_0_r := eq_mul_0_r.
 Theorem lt_0_mul n m : 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof.
 split; [intro H | intros [[H1 H2] | [H1 H2]]].
-destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
-[| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |];
-(destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
-[| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]);
-try (left; now split); try (right; now split).
-assert (H3 : n * m < 0) by now apply mul_neg_pos.
-exfalso; now apply (lt_asymm (n * m) 0).
-assert (H3 : n * m < 0) by now apply mul_pos_neg.
-exfalso; now apply (lt_asymm (n * m) 0).
-now apply mul_pos_pos. now apply mul_neg_neg.
+- destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
+    [| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |];
+    (destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
+     [| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]);
+    try (left; now split); try (right; now split).
+  + assert (H3 : n * m < 0) by now apply mul_neg_pos.
+    exfalso; now apply (lt_asymm (n * m) 0).
+  + assert (H3 : n * m < 0) by now apply mul_pos_neg.
+    exfalso; now apply (lt_asymm (n * m) 0).
+- now apply mul_pos_pos. - now apply mul_neg_neg.
 Qed.
 
 Theorem square_lt_mono_nonneg : forall n m, 0 <= n -> n < m -> n * n < m * m.
@@ -304,38 +305,38 @@ other variable *)
 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) as [LT|LE]; trivial.
-apply square_le_mono_nonneg in LE; order.
+- now apply lt_le_trans with 0.
+- 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) as [LE|LT]; trivial.
-apply square_lt_mono_nonneg in LT; order.
+- apply lt_le_incl; now apply lt_le_trans with 0.
+- 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.
 Proof.
 intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two).
-rewrite two_succ. nzsimpl. now rewrite le_succ_l.
-order'.
+- rewrite two_succ. nzsimpl. now rewrite le_succ_l.
+- order'.
 Qed.
 
 Lemma add_le_mul : forall a b, 1<a -> 1<b -> a+b <= a*b.
 Proof.
  assert (AUX : forall a b, 0<a -> 0<b -> (S a)+(S b) <= (S a)*(S b)).
-  intros a b Ha Hb.
-  nzsimpl. rewrite <- succ_le_mono. apply le_succ_l.
-  rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b).
-  apply add_lt_mono_r.
-  now apply mul_pos_pos.
- intros a b Ha Hb.
- assert (Ha' := lt_succ_pred 1 a Ha).
- assert (Hb' := lt_succ_pred 1 b Hb).
- rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order.
+ - intros a b Ha Hb.
+   nzsimpl. rewrite <- succ_le_mono. apply le_succ_l.
+   rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b).
+   apply add_lt_mono_r.
+   now apply mul_pos_pos.
+ - intros a b Ha Hb.
+   assert (Ha' := lt_succ_pred 1 a Ha).
+   assert (Hb' := lt_succ_pred 1 b Hb).
+   rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order.
 Qed.
 
 (** A few results about squares *)
@@ -343,25 +344,25 @@ Qed.
 Lemma square_nonneg : forall a, 0 <= a * a.
 Proof.
  intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0).
- now apply mul_le_mono_nonpos_l.
- apply mul_le_mono_nonneg_l; order.
+ - now apply mul_le_mono_nonpos_l.
+ - apply mul_le_mono_nonneg_l; order.
 Qed.
 
 Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b.
 Proof.
  assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b).
-  intros a b (Ha,H).
-  destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
-  rewrite EQ.
-  rewrite 2 mul_add_distr_r.
-  rewrite !add_assoc. apply add_le_mono_r.
-  rewrite add_comm. apply add_le_mono_l.
-  apply mul_le_mono_nonneg_l; trivial. order.
- intros a b Ha Hb.
- destruct (le_gt_cases a b).
- apply AUX; split; order.
- rewrite (add_comm (b*a)), (add_comm (a*a)).
- apply AUX; split; order.
+ - intros a b (Ha,H).
+   destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
+   rewrite EQ.
+   rewrite 2 mul_add_distr_r.
+   rewrite !add_assoc. apply add_le_mono_r.
+   rewrite add_comm. apply add_le_mono_l.
+   apply mul_le_mono_nonneg_l; trivial. order.
+ - intros a b Ha Hb.
+   destruct (le_gt_cases a b).
+   + apply AUX; split; order.
+   + rewrite (add_comm (b*a)), (add_comm (a*a)).
+     apply AUX; split; order.
 Qed.
 
 Lemma add_square_le : forall a b, 0<=a -> 0<=b ->
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 60e1123b35..89bc5cfecb 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -60,19 +60,19 @@ Qed.
 Theorem nle_succ_diag_l : forall n, ~ S n <= n.
 Proof.
 intros n H; le_elim H.
-false_hyp H nlt_succ_diag_l. false_hyp H neq_succ_diag_l.
++ false_hyp H nlt_succ_diag_l. + false_hyp H neq_succ_diag_l.
 Qed.
 
 Theorem le_succ_l : forall n m, S n <= m <-> n < m.
 Proof.
 intro n; nzinduct m n.
-split; intro H. false_hyp H nle_succ_diag_l. false_hyp H lt_irrefl.
-intro m.
-rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd.
-rewrite or_cancel_r.
-reflexivity.
-intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l.
-intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl.
+- split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl.
+- intro m.
+  rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd.
+  rewrite or_cancel_r.
+  + reflexivity.
+  + intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l.
+  + intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl.
 Qed.
 
 (** Trichotomy *)
@@ -80,8 +80,8 @@ Qed.
 Theorem le_gt_cases : forall n m, n <= m \/ n > m.
 Proof.
 intros n m; nzinduct n m.
-left; apply le_refl.
-intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition.
+- left; apply le_refl.
+- intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition.
 Qed.
 
 Theorem lt_trichotomy : forall n m,  n < m \/ n == m \/ m < n.
@@ -96,14 +96,14 @@ Notation lt_eq_gt_cases := lt_trichotomy (only parsing).
 Theorem lt_asymm : forall n m, n < m -> ~ m < n.
 Proof.
 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.
-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.
-rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l.
+- 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.
+    * 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.
+    * rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l.
 Qed.
 
 Notation lt_ngt := lt_asymm (only parsing).
@@ -111,13 +111,15 @@ Notation lt_ngt := lt_asymm (only parsing).
 Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
 Proof.
 intros n m p; nzinduct p m.
-intros _ H; false_hyp H lt_irrefl.
-intro p. rewrite 2 lt_succ_r.
-split; intros H H1 H2.
-apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1].
-assert (n <= p) as H3 by (auto using lt_le_incl).
-le_elim H3. assumption. rewrite <- H3 in H2.
-elim (lt_asymm n m); auto.
+- intros _ H; false_hyp H lt_irrefl.
+- intro p. rewrite 2 lt_succ_r.
+  split; intros H H1 H2.
+  + apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1].
+  + assert (n <= p) as H3 by (auto using lt_le_incl).
+    le_elim H3.
+    * assumption.
+    * rewrite <- H3 in H2.
+      elim (lt_asymm n m); auto.
 Qed.
 
 Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
@@ -130,16 +132,16 @@ Qed.
 (** Some type classes about order *)
 
 Instance lt_strorder : StrictOrder lt.
-Proof. split. exact lt_irrefl. exact lt_trans. Qed.
+Proof. split. - exact lt_irrefl. - exact lt_trans. Qed.
 
 Instance le_preorder : PreOrder le.
-Proof. split. exact le_refl. exact le_trans. Qed.
+Proof. split. - exact le_refl. - exact le_trans. Qed.
 
 Instance le_partialorder : PartialOrder _ le.
 Proof.
 intros x y. compute. split.
-intro EQ; now rewrite EQ.
-rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y.
+- intro EQ; now rewrite EQ.
+- rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y.
 Qed.
 
 (** We know enough now to benefit from the generic [order] tactic. *)
@@ -246,7 +248,7 @@ Qed.
 
 Theorem lt_0_2 : 0 < 2.
 Proof.
-transitivity 1. apply lt_0_1. apply lt_1_2.
+  transitivity 1. - apply lt_0_1. - apply lt_1_2.
 Qed.
 
 Theorem le_0_2 : 0 <= 2.
@@ -300,9 +302,9 @@ Qed.
 Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
-destruct (eq_decidable n m) as [H1 | H1].
-assumption. false_hyp H1 H.
-intro H1; now apply H1.
+- destruct (eq_decidable n m) as [H1 | H1].
+  + assumption. + false_hyp H1 H.
+- intro H1; now apply H1.
 Qed.
 
 Theorem le_ngt : forall n m, n <= m <-> ~ n > m.
@@ -321,8 +323,8 @@ Qed.
 Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.
 Proof.
 intros n m; split; intro H.
-destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
-intro H1; false_hyp H H1.
+- destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
+- intro H1; false_hyp H H1.
 Qed.
 
 Theorem nle_gt : forall n m, ~ n <= m <-> n > m.
@@ -341,8 +343,8 @@ Qed.
 Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m.
 Proof.
 intros n m; split; intro H.
-destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
-intro H1; false_hyp H H1.
+- destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
+- intro H1; false_hyp H H1.
 Qed.
 
 Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m.
@@ -361,18 +363,18 @@ Lemma lt_exists_pred_strong :
   forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k.
 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].
-now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2].
-apply IH. assumption. now apply le_le_succ_r.
+- order.
+- intro n; split; intros IH m H1 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.
 
 Theorem lt_exists_pred :
   forall z n, z < n -> exists k, n == S k /\ z <= k.
 Proof.
 intros z n H; apply lt_exists_pred_strong with (z := z) (n := n).
-assumption. apply le_refl.
+- assumption. - apply le_refl.
 Qed.
 
 Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n.
@@ -404,18 +406,19 @@ Let right_step'' := forall n, A' n <-> A' (S n).
 Lemma rs_rs' :  A z -> right_step -> right_step'.
 Proof.
 intros Az RS n H1 H2.
-le_elim H1. apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]].
-rewrite H3. apply RS; trivial. apply H2; trivial.
-rewrite H3; apply lt_succ_diag_r.
-rewrite <- H1; apply Az.
+le_elim H1.
+- apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]].
+  rewrite H3. apply RS; trivial. apply H2; trivial.
+  rewrite H3; apply lt_succ_diag_r.
+- rewrite <- H1; apply Az.
 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;
-[now apply H1 | rewrite H3 in *; now apply RS'].
-apply H1; [assumption | now apply lt_lt_succ_r].
+- 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.
@@ -444,10 +447,12 @@ Theorem right_induction' :
 Proof.
 intros L R n.
 destruct (lt_trichotomy n z) as [H | [H | H]].
-apply L; now apply lt_le_incl.
-apply L; now apply eq_le_incl.
-apply right_induction. apply L; now apply eq_le_incl. assumption.
-now apply lt_le_incl.
+- apply L; now apply lt_le_incl.
+- apply L; now apply eq_le_incl.
+- apply right_induction.
+  + apply L; now apply eq_le_incl.
+  + assumption.
+  + now apply lt_le_incl.
 Qed.
 
 Theorem strong_right_induction' :
@@ -455,9 +460,10 @@ Theorem strong_right_induction' :
 Proof.
 intros L R n.
 destruct (lt_trichotomy n z) as [H | [H | H]].
-apply L; now apply lt_le_incl.
-apply L; now apply eq_le_incl.
-apply strong_right_induction. assumption. now apply lt_le_incl.
+- apply L; now apply lt_le_incl.
+- apply L; now apply eq_le_incl.
+- apply strong_right_induction.
+  + assumption. + now apply lt_le_incl.
 Qed.
 
 End RightInduction.
@@ -472,17 +478,17 @@ 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].
-rewrite H1; apply Az.
+- 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.
-le_elim H3.
-apply le_succ_l in H3. now apply H1.
-rewrite <- H3 in *; now apply LS'.
+- 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.
+  + rewrite <- H3 in *; now apply LS'.
 Qed.
 
 Lemma lbase : A' (S z).
@@ -512,10 +518,12 @@ Theorem left_induction' :
 Proof.
 intros R L n.
 destruct (lt_trichotomy n z) as [H | [H | H]].
-apply left_induction. apply R. now apply eq_le_incl. assumption.
-now apply lt_le_incl.
-rewrite H; apply R; now apply eq_le_incl.
-apply R; now apply lt_le_incl.
+- apply left_induction.
+  + apply R. now apply eq_le_incl.
+  + assumption.
+  + now apply lt_le_incl.
+- rewrite H; apply R; now apply eq_le_incl.
+- apply R; now apply lt_le_incl.
 Qed.
 
 Theorem strong_left_induction' :
@@ -523,9 +531,9 @@ Theorem strong_left_induction' :
 Proof.
 intros R L n.
 destruct (lt_trichotomy n z) as [H | [H | H]].
-apply strong_left_induction; auto. now apply lt_le_incl.
-rewrite H; apply R; now apply eq_le_incl.
-apply R; now apply lt_le_incl.
+- apply strong_left_induction; auto. now apply lt_le_incl.
+- rewrite H; apply R; now apply eq_le_incl.
+- apply R; now apply lt_le_incl.
 Qed.
 
 End LeftInduction.
@@ -538,9 +546,9 @@ Theorem order_induction :
 Proof.
 intros Az RS LS n.
 destruct (lt_trichotomy n z) as [H | [H | H]].
-now apply left_induction; [| | apply lt_le_incl].
-now rewrite H.
-now apply right_induction; [| | apply lt_le_incl].
+- now apply left_induction; [| | apply lt_le_incl].
+- now rewrite H.
+- now apply right_induction; [| | apply lt_le_incl].
 Qed.
 
 Theorem order_induction' :
@@ -622,21 +630,24 @@ Theorem lt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
 apply strong_right_induction' with (z := z).
-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.
-intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
+- 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.
+- intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
 Theorem gt_wf : well_founded Rgt.
 Proof.
 unfold well_founded.
 apply strong_left_induction' with (z := z).
-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.
-intros n H1 H2; constructor; intros m [H3 H4].
-apply H2. assumption. now apply le_succ_l.
+- 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.
+- intros n H1 H2; constructor; intros m [H3 H4].
+  apply H2.
+  + assumption. + now apply le_succ_l.
 Qed.
 
 End WF.
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 93d99f08f5..84b8a96e64 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -48,20 +48,20 @@ Qed.
 Lemma Even_or_Odd : forall x, Even x \/ Odd x.
 Proof.
  nzinduct x.
- left. exists 0. now nzsimpl.
- intros x.
- split; intros [(y,H)|(y,H)].
- right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl'.
- right.
- assert (LT : exists z, z<y).
-  destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x].
-  rewrite <- le_succ_l, H. nzsimpl'.
-  rewrite <- (add_0_r y) at 3. now apply add_le_mono_l.
- destruct LT as (z,LT).
- destruct (lt_exists_pred z y LT) as (y' & Hy' & _).
- exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'.
- left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
+ - left. exists 0. now nzsimpl.
+ - intros x.
+   split; intros [(y,H)|(y,H)].
+   + right. exists y. rewrite H. now nzsimpl.
+   + left. exists (S y). rewrite H. now nzsimpl'.
+   + right.
+     assert (LT : exists z, z<y).
+     * destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x].
+       rewrite <- le_succ_l, H. nzsimpl'.
+       rewrite <- (add_0_r y) at 3. now apply add_le_mono_l.
+     * destruct LT as (z,LT).
+       destruct (lt_exists_pred z y LT) as (y' & Hy' & _).
+       exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'.
+   + left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
 Qed.
 
 Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
@@ -80,16 +80,16 @@ Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
 Proof.
 intros x (y,E) (z,O). rewrite O in E; clear O.
 destruct (le_gt_cases y z) as [LE|GT].
-generalize (double_below _ _ LE); order.
-generalize (double_above _ _ GT); order.
+- generalize (double_below _ _ LE); order.
+- generalize (double_above _ _ GT); order.
 Qed.
 
 Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
 Proof.
  intros.
  destruct (Even_or_Odd n) as [H|H].
- rewrite <- even_spec in H. now rewrite H.
- rewrite <- odd_spec in H. now rewrite H, orb_true_r.
+ - rewrite <- even_spec in H. now rewrite H.
+ - rewrite <- odd_spec in H. now rewrite H, orb_true_r.
 Qed.
 
 Lemma negb_odd : forall n, negb (odd n) = even n.
@@ -142,8 +142,8 @@ Qed.
 Lemma Odd_succ : forall n, Odd (S n) <-> Even n.
 Proof.
  split; intros (m,H).
- exists m. apply succ_inj. now rewrite add_1_r in H.
- exists m. rewrite add_1_r. now f_equiv.
+ - exists m. apply succ_inj. now rewrite add_1_r in H.
+ - exists m. rewrite add_1_r. now f_equiv.
 Qed.
 
 Lemma odd_succ : forall n, odd (S n) = even n.
@@ -192,10 +192,10 @@ Proof.
  case_eq (even n); case_eq (even m);
   rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
   intros (m',Hm) (n',Hn).
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
- exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
+ - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
+ - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
+ - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
+ - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
 Qed.
 
 Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
@@ -210,14 +210,14 @@ Lemma even_mul : forall n m, even (mul n m) = even n || even m.
 Proof.
  intros.
  case_eq (even n); simpl; rewrite ?even_spec.
- intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
- case_eq (even m); simpl; rewrite ?even_spec.
- intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
- (* odd / odd *)
- rewrite <- !negb_true_iff, !negb_even, !odd_spec.
- intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
- rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
- now rewrite add_shuffle1, add_assoc, !mul_assoc.
+ - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
+ - case_eq (even m); simpl; rewrite ?even_spec.
+   + intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
+     (* odd / odd *)
+   + rewrite <- !negb_true_iff, !negb_even, !odd_spec.
+     intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
+     rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
+     now rewrite add_shuffle1, add_assoc, !mul_assoc.
 Qed.
 
 Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index a1310667e1..830540bc66 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -60,8 +60,8 @@ Lemma pow_0_l' : forall a, a~=0 -> 0^a == 0.
 Proof.
  intros a Ha.
  destruct (lt_trichotomy a 0) as [LT|[EQ|GT]]; try order.
- now rewrite pow_neg_r.
- now apply pow_0_l.
+ - now rewrite pow_neg_r.
+ - now apply pow_0_l.
 Qed.
 
 Lemma pow_1_r : forall a, a^1 == a.
@@ -71,9 +71,9 @@ Qed.
 
 Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.
 Proof.
- apply le_ind; intros. solve_proper.
- now nzsimpl.
- now nzsimpl.
+  apply le_ind; intros. - solve_proper.
+  - now nzsimpl.
+  - now nzsimpl.
 Qed.
 
 Hint Rewrite pow_1_r pow_1_l : nz.
@@ -90,12 +90,12 @@ 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_proper.
- rewrite pow_0_r. order'.
- clear b Hb. intros b Hb IH.
- rewrite pow_succ_r by trivial.
- intros H. apply eq_mul_0 in H. destruct H; trivial.
- now apply IH.
+ - solve_proper.
+ - rewrite pow_0_r. order'.
+ - clear b Hb. intros b Hb IH.
+   rewrite pow_succ_r by trivial.
+   intros H. apply eq_mul_0 in H. destruct H; trivial.
+   now apply IH.
 Qed.
 
 Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0.
@@ -106,13 +106,13 @@ Qed.
 Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0).
 Proof.
  intros a b. split.
- intros H.
- destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]].
- now left.
- rewrite Hb, pow_0_r in H; order'.
- right. split; trivial. apply pow_eq_0 with b; order.
- intros [Hb|[Hb Ha]]. now rewrite pow_neg_r.
- rewrite Ha. apply pow_0_l'. order.
+ - intros H.
+   destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]].
+   + now left.
+   + rewrite Hb, pow_0_r in H; order'.
+   + right. split; trivial. apply pow_eq_0 with b; order.
+ - intros [Hb|[Hb Ha]]. + now rewrite pow_neg_r.
+   + rewrite Ha. apply pow_0_l'. order.
 Qed.
 
 (** Power and addition, multiplication *)
@@ -120,12 +120,12 @@ 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_proper.
- now nzsimpl.
- clear b Hb. intros b Hb IH Hc.
- nzsimpl; trivial.
- rewrite IH; trivial. apply mul_assoc.
- now apply add_nonneg_nonneg.
+  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.
+    + rewrite IH; trivial. apply mul_assoc.
+    + now apply add_nonneg_nonneg.
 Qed.
 
 Lemma pow_mul_l : forall a b c,
@@ -133,23 +133,23 @@ Lemma pow_mul_l : forall a b c,
 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_proper.
- now nzsimpl.
- clear c Hc. intros c Hc IH.
- nzsimpl; trivial.
- rewrite IH; trivial. apply mul_shuffle1.
+ - rewrite !(pow_neg_r _ _ Hc). now nzsimpl.
+ - apply le_ind with (4:=Hc). + solve_proper.
+   + now nzsimpl.
+   + clear c Hc. intros c Hc IH.
+     nzsimpl; trivial.
+     rewrite IH; trivial. apply mul_shuffle1.
 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_proper.
- intros. now nzsimpl.
- clear b Hb. intros b Hb IH Hc.
- nzsimpl; trivial.
- rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm.
- now apply mul_nonneg_nonneg.
+  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.
+    rewrite pow_add_r, IH, pow_mul_l; trivial. + apply mul_comm.
+    + now apply mul_nonneg_nonneg.
 Qed.
 
 (** Positivity *)
@@ -158,67 +158,67 @@ Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.
 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_proper.
- nzsimpl; order'.
- clear b Hb. intros b Hb IH.
- nzsimpl; trivial. now apply mul_nonneg_nonneg.
+ - now rewrite !(pow_neg_r _ _ Hb).
+ - apply le_ind with (4:=Hb). + solve_proper.
+   + nzsimpl; order'.
+   + clear b Hb. intros b Hb IH.
+     nzsimpl; trivial. now apply mul_nonneg_nonneg.
 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_proper.
- nzsimpl; order'.
- clear b Hb. intros b Hb IH.
- nzsimpl; trivial. now apply mul_pos_pos.
+  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.
 Qed.
 
 (** Monotonicity *)
 
 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_proper.
- intros (Ha,H). nzsimpl; trivial; order.
- clear c Hc. intros c Hc IH (Ha,H).
- nzsimpl; try order.
- apply mul_lt_mono_nonneg; trivial.
- apply pow_nonneg; try order.
- apply IH. now split.
+  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.
+    apply mul_lt_mono_nonneg; trivial.
+    + apply pow_nonneg; try order.
+    + apply IH. now split.
 Qed.
 
 Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c.
 Proof.
  intros a b c (Ha,H).
  destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]].
- rewrite !(pow_neg_r _ _ Hc); now nzsimpl.
- rewrite Hc; now nzsimpl.
- apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H].
- apply lt_le_incl, pow_lt_mono_l; now try split.
+ - rewrite !(pow_neg_r _ _ Hc); now nzsimpl.
+ - rewrite Hc; now nzsimpl.
+ - apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H].
+   apply lt_le_incl, pow_lt_mono_l; now try split.
 Qed.
 
 Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b).
 Proof.
  intros a b Ha. split; intros Hb.
- rewrite <- (pow_1_l b) by order.
- apply pow_lt_mono_l; try split; order'.
- destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial.
- rewrite pow_neg_r in Hb; order'.
- rewrite H, pow_0_r in Hb. order.
+ - rewrite <- (pow_1_l b) by order.
+   apply pow_lt_mono_l; try split; order'.
+ - destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial.
+   + rewrite pow_neg_r in Hb; order'.
+   + rewrite H, pow_0_r in Hb. order.
 Qed.
 
 Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=c -> b<c -> a^b < a^c.
 Proof.
  intros a b c Ha Hc H.
  destruct (lt_ge_cases b 0) as [Hb|Hb].
- rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'.
- assert (H' : b<=c) by order.
- destruct (le_exists_sub _ _ H') as (d & EQ & Hd).
- rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1.
- apply mul_lt_mono_pos_r.
- apply pow_pos_nonneg; order'.
- apply pow_gt_1; trivial.
- apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial.
-  rewrite <- EQ' in *. rewrite add_0_l in EQ. order.
+ - rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'.
+ - assert (H' : b<=c) by order.
+   destruct (le_exists_sub _ _ H') as (d & EQ & Hd).
+   rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1.
+   apply mul_lt_mono_pos_r.
+   + apply pow_pos_nonneg; order'.
+   + apply pow_gt_1; trivial.
+     apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial.
+     rewrite <- EQ' in *. rewrite add_0_l in EQ. order.
 Qed.
 
 (** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
@@ -227,20 +227,20 @@ Lemma pow_le_mono_r : forall a b c, 0<a -> b<=c -> a^b <= a^c.
 Proof.
  intros a b c Ha H.
  destruct (lt_ge_cases b 0) as [Hb|Hb].
- rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order.
- apply le_succ_l in Ha; rewrite <- one_succ in Ha.
- apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
- apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
- apply lt_le_incl, pow_lt_mono_r; order.
- nzsimpl; order.
+ - rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order.
+ - apply le_succ_l in Ha; rewrite <- one_succ in Ha.
+   apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
+   + apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
+     apply lt_le_incl, pow_lt_mono_r; order.
+   + nzsimpl; order.
 Qed.
 
 Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d ->
  a^b <= c^d.
 Proof.
  intros. transitivity (a^d).
- apply pow_le_mono_r; intuition order.
- apply pow_le_mono_l; intuition order.
+ - apply pow_le_mono_r; intuition order.
+ - apply pow_le_mono_l; intuition order.
 Qed.
 
 Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
@@ -249,10 +249,10 @@ Proof.
  intros a b c d (Ha,Hac) (Hb,Hbd).
  apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
- transitivity (a^d).
- apply pow_lt_mono_r; intuition order.
- apply pow_lt_mono_l; try split; order'.
- nzsimpl; try order. apply pow_gt_1; order.
+ - transitivity (a^d).
+   + apply pow_lt_mono_r; intuition order.
+   + apply pow_lt_mono_l; try split; order'.
+ - nzsimpl; try order. apply pow_gt_1; order.
 Qed.
 
 (** Injectivity *)
@@ -262,10 +262,10 @@ Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c ->
 Proof.
  intros a b c Ha Hb Hc EQ.
  destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial.
- assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial).
- order.
- assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
- order.
+ - assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial).
+   order.
+ - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
+   order.
 Qed.
 
 Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c ->
@@ -273,10 +273,10 @@ Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c ->
 Proof.
  intros a b c Ha Hb Hc EQ.
  destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial.
- assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial).
- order.
- assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial).
- order.
+ - assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial).
+   order.
+ - assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial).
+   order.
 Qed.
 
 (** Monotonicity results, both ways *)
@@ -286,10 +286,10 @@ Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
 Proof.
  intros a b c Ha Hb Hc.
  split; intro LT.
- apply pow_lt_mono_l; try split; trivial.
- destruct (le_gt_cases b a) as [LE|GT]; trivial.
- assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order).
- order.
+ - apply pow_lt_mono_l; try split; trivial.
+ - destruct (le_gt_cases b a) as [LE|GT]; trivial.
+   assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order).
+   order.
 Qed.
 
 Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
@@ -297,10 +297,10 @@ Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
 Proof.
  intros a b c Ha Hb Hc.
  split; intro LE.
- apply pow_le_mono_l; try split; trivial.
- destruct (le_gt_cases a b) as [LE'|GT]; trivial.
- assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
- order.
+ - apply pow_le_mono_l; try split; trivial.
+ - destruct (le_gt_cases a b) as [LE'|GT]; trivial.
+   assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
+   order.
 Qed.
 
 Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c ->
@@ -308,10 +308,10 @@ Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c ->
 Proof.
  intros a b c Ha Hc.
  split; intro LT.
- now apply pow_lt_mono_r.
- destruct (le_gt_cases c b) as [LE|GT]; trivial.
- assert (a^c <= a^b) by (apply pow_le_mono_r; order').
- order.
+ - now apply pow_lt_mono_r.
+ - destruct (le_gt_cases c b) as [LE|GT]; trivial.
+   assert (a^c <= a^b) by (apply pow_le_mono_r; order').
+   order.
 Qed.
 
 Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c ->
@@ -319,26 +319,26 @@ Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c ->
 Proof.
  intros a b c Ha Hc.
  split; intro LE.
- apply pow_le_mono_r; order'.
- destruct (le_gt_cases b c) as [LE'|GT]; trivial.
- assert (a^c < a^b) by (apply pow_lt_mono_r; order').
- order.
+ - apply pow_le_mono_r; order'.
+ - destruct (le_gt_cases b c) as [LE'|GT]; trivial.
+   assert (a^c < a^b) by (apply pow_lt_mono_r; order').
+   order.
 Qed.
 
 (** For any a>1, the a^x function is above the identity function *)
 
 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_proper.
- nzsimpl. order'.
- clear b Hb. intros b Hb IH. nzsimpl; trivial.
- rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha.
- transitivity (2*(S b)).
-  nzsimpl'. rewrite <- 2 succ_le_mono.
-  rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
- apply mul_le_mono_nonneg; trivial.
- order'.
- now apply lt_le_incl, lt_succ_r.
+  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.
+    transitivity (2*(S b)).
+    + nzsimpl'. rewrite <- 2 succ_le_mono.
+      rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
+    + apply mul_le_mono_nonneg; trivial.
+      * order'.
+      * now apply lt_le_incl, lt_succ_r.
 Qed.
 
 (** Someday, we should say something about the full Newton formula.
@@ -349,22 +349,22 @@ 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_proper.
- nzsimpl; order.
- clear c Hc. intros c Hc IH.
- assert (0<=c) by order'.
- nzsimpl; trivial.
- transitivity ((a+b)*(a^c + b^c)).
- rewrite mul_add_distr_r, !mul_add_distr_l.
- apply add_le_mono.
- rewrite <- add_0_r at 1. apply add_le_mono_l.
-  apply mul_nonneg_nonneg; trivial.
-  apply pow_nonneg; trivial.
- rewrite <- add_0_l at 1. apply add_le_mono_r.
-  apply mul_nonneg_nonneg; trivial.
-  apply pow_nonneg; trivial.
- apply mul_le_mono_nonneg_l; trivial.
- now apply add_nonneg_nonneg.
+  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'.
+    nzsimpl; trivial.
+    transitivity ((a+b)*(a^c + b^c)).
+    + rewrite mul_add_distr_r, !mul_add_distr_l.
+      apply add_le_mono.
+      * rewrite <- add_0_r at 1. apply add_le_mono_l.
+        apply mul_nonneg_nonneg; trivial.
+        apply pow_nonneg; trivial.
+      * rewrite <- add_0_l at 1. apply add_le_mono_r.
+        apply mul_nonneg_nonneg; trivial.
+        apply pow_nonneg; trivial.
+    + apply mul_le_mono_nonneg_l; trivial.
+      now apply add_nonneg_nonneg.
 Qed.
 
 (** This upper bound can also be seen as a convexity proof for x^c :
@@ -377,37 +377,37 @@ Proof.
  assert (aux : forall a b c, 0<=a<=b -> 0<c ->
          (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)).
  (* begin *)
-  intros a b c (Ha,H) Hc.
-  rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'.
-  rewrite <- !add_assoc. apply add_le_mono_l.
-  rewrite !add_assoc. apply add_le_mono_r.
-  destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
-  rewrite EQ.
-  rewrite 2 mul_add_distr_r.
-  rewrite !add_assoc. apply add_le_mono_r.
-  rewrite add_comm. apply add_le_mono_l.
-  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_proper.
- nzsimpl; order.
- clear c Hc. intros c Hc IH.
- assert (0<=c) by order.
- nzsimpl; trivial.
- transitivity ((a+b)*(2^(pred c) * (a^c + b^c))).
- apply mul_le_mono_nonneg_l; trivial.
- now apply add_nonneg_nonneg.
- rewrite mul_assoc. rewrite (mul_comm (a+b)).
- assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order').
- assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l).
- assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order).
- rewrite EQ', <- !mul_assoc.
- apply mul_le_mono_nonneg_l.
- apply pow_nonneg; order'.
- destruct (le_gt_cases a b).
- apply aux; try split; order'.
- rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)).
- apply aux; try split; order'.
+ - intros a b c (Ha,H) Hc.
+   rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'.
+   rewrite <- !add_assoc. apply add_le_mono_l.
+   rewrite !add_assoc. apply add_le_mono_r.
+   destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
+   rewrite EQ.
+   rewrite 2 mul_add_distr_r.
+   rewrite !add_assoc. apply add_le_mono_r.
+   rewrite add_comm. apply add_le_mono_l.
+   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_proper.
+   + nzsimpl; order.
+   + clear c Hc. intros c Hc IH.
+     assert (0<=c) by order.
+     nzsimpl; trivial.
+     transitivity ((a+b)*(2^(pred c) * (a^c + b^c))).
+     * apply mul_le_mono_nonneg_l; trivial.
+       now apply add_nonneg_nonneg.
+     * rewrite mul_assoc. rewrite (mul_comm (a+b)).
+       assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order').
+       assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l).
+       assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order).
+       rewrite EQ', <- !mul_assoc.
+       apply mul_le_mono_nonneg_l.
+       -- apply pow_nonneg; order'.
+       -- destruct (le_gt_cases a b).
+          ++ apply aux; try split; order'.
+          ++ rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)).
+             apply aux; try split; order'.
 Qed.
 
 End NZPowProp.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index c2d2c4ae19..85ed71b8a4 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -49,18 +49,18 @@ Proof.
  intros b LT.
  destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso.
  assert ((S b)² < b²).
-  rewrite mul_succ_l, <- (add_0_r b²).
-  apply add_lt_le_mono.
-  apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r.
-  now apply le_succ_l.
- order.
+ - rewrite mul_succ_l, <- (add_0_r b²).
+   apply add_lt_le_mono.
+   + apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r.
+   + now apply le_succ_l.
+ - order.
 Qed.
 
 Lemma sqrt_nonneg : forall a, 0<=√a.
 Proof.
  intros. destruct (lt_ge_cases a 0) as [Ha|Ha].
- now rewrite (sqrt_neg _ Ha).
- apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order.
+ - now rewrite (sqrt_neg _ Ha).
+ - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order.
 Qed.
 
 (** The spec of sqrt indeed determines it *)
@@ -73,12 +73,12 @@ Proof.
  assert (Ha': 0<=√a) by now apply sqrt_nonneg.
  destruct (sqrt_spec a Ha) as (LEa,LTa).
  assert (b <= √a).
-  apply lt_succ_r, square_lt_simpl_nonneg; [|order].
-  now apply lt_le_incl, lt_succ_r.
- assert (√a <= b).
-  apply lt_succ_r, square_lt_simpl_nonneg; [|order].
-  now apply lt_le_incl, lt_succ_r.
- order.
+ - apply lt_succ_r, square_lt_simpl_nonneg; [|order].
+   now apply lt_le_incl, lt_succ_r.
+ - assert (√a <= b).
+   + apply lt_succ_r, square_lt_simpl_nonneg; [|order].
+     now apply lt_le_incl, lt_succ_r.
+   + order.
 Qed.
 
 (** Hence sqrt is a morphism *)
@@ -87,9 +87,9 @@ Instance sqrt_wd : Proper (eq==>eq) sqrt.
 Proof.
  intros x x' Hx.
  destruct (lt_ge_cases x 0) as [H|H].
- rewrite 2 sqrt_neg; trivial. reflexivity.
- now rewrite <- Hx.
- apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec.
+ - rewrite 2 sqrt_neg; trivial. + reflexivity.
+   + now rewrite <- Hx.
+ - apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec.
 Qed.
 
 (** An alternate specification *)
@@ -101,11 +101,11 @@ Proof.
  destruct (sqrt_spec _ Ha) as (LE,LT).
  destruct (le_exists_sub _ _ LE) as (r & Hr & Hr').
  exists r.
- split. now rewrite add_comm.
- split. trivial.
- apply (add_le_mono_r _ _ (√a)²).
- rewrite <- Hr, add_comm.
- generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc.
+ split. - now rewrite add_comm.
+ - split. + trivial.
+   + apply (add_le_mono_r _ _ (√a)²).
+     rewrite <- Hr, add_comm.
+     generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc.
 Qed.
 
 Lemma sqrt_unique' : forall a b c, 0<=c<=2*b ->
@@ -115,10 +115,10 @@ Proof.
  apply sqrt_unique.
  rewrite EQ.
  split.
- rewrite <- add_0_r at 1. now apply add_le_mono_l.
- nzsimpl. apply lt_succ_r.
- rewrite <- add_assoc. apply add_le_mono_l.
- generalize H; now nzsimpl'.
+ - rewrite <- add_0_r at 1. now apply add_le_mono_l.
+ - nzsimpl. apply lt_succ_r.
+   rewrite <- add_assoc. apply add_le_mono_l.
+   generalize H; now nzsimpl'.
 Qed.
 
 (** Sqrt is exact on squares *)
@@ -127,7 +127,7 @@ Lemma sqrt_square : forall a, 0<=a -> √(a²) == a.
 Proof.
  intros a Ha.
  apply sqrt_unique' with 0.
- split. order. apply mul_nonneg_nonneg; order'. now nzsimpl.
+ - split. + order. + apply mul_nonneg_nonneg; order'. - now nzsimpl.
 Qed.
 
 (** Sqrt and predecessors of squares *)
@@ -138,14 +138,14 @@ Proof.
  apply sqrt_unique.
  assert (EQ := lt_succ_pred 0 a Ha).
  rewrite EQ. split.
- apply lt_succ_r.
- rewrite (lt_succ_pred 0).
- assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ).
- assert (P a < a) by (now rewrite <- le_succ_l, EQ).
- apply mul_lt_mono_nonneg; trivial.
- now apply mul_pos_pos.
- apply le_succ_l.
- rewrite (lt_succ_pred 0). reflexivity. now apply mul_pos_pos.
+ - apply lt_succ_r.
+   rewrite (lt_succ_pred 0).
+   + assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ).
+     assert (P a < a) by (now rewrite <- le_succ_l, EQ).
+     apply mul_lt_mono_nonneg; trivial.
+   + now apply mul_pos_pos.
+ - apply le_succ_l.
+   rewrite (lt_succ_pred 0). + reflexivity. + now apply mul_pos_pos.
 Qed.
 
 (** Sqrt is a monotone function (but not a strict one) *)
@@ -154,13 +154,13 @@ Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b.
 Proof.
  intros a b Hab.
  destruct (lt_ge_cases a 0) as [Ha|Ha].
- rewrite (sqrt_neg _ Ha). apply sqrt_nonneg.
- assert (Hb : 0 <= b) by order.
- destruct (sqrt_spec a Ha) as (LE,_).
- destruct (sqrt_spec b Hb) as (_,LT).
- apply lt_succ_r.
- apply square_lt_simpl_nonneg; try order.
- now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+ - rewrite (sqrt_neg _ Ha). apply sqrt_nonneg.
+ - assert (Hb : 0 <= b) by order.
+   destruct (sqrt_spec a Ha) as (LE,_).
+   destruct (sqrt_spec b Hb) as (_,LT).
+   apply lt_succ_r.
+   apply square_lt_simpl_nonneg; try order.
+   now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
 Qed.
 
 (** No reverse result for <=, consider for instance √2 <= √1 *)
@@ -169,16 +169,16 @@ Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
 Proof.
  intros a b H.
  destruct (lt_ge_cases b 0) as [Hb|Hb].
- rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order.
- destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|].
- destruct (sqrt_spec a Ha) as (_,LT).
- destruct (sqrt_spec b Hb) as (LE,_).
- apply le_succ_l in H.
- assert ((S (√a))² <= (√b)²).
-  apply mul_le_mono_nonneg; trivial.
-  now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
-  now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
- order.
+ - rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order.
+ - destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|].
+   destruct (sqrt_spec a Ha) as (_,LT).
+   destruct (sqrt_spec b Hb) as (LE,_).
+   apply le_succ_l in H.
+   assert ((S (√a))² <= (√b)²).
+   + apply mul_le_mono_nonneg; trivial.
+     * now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+     * now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+   + order.
 Qed.
 
 (** When left side is a square, we have an equivalence for <= *)
@@ -186,11 +186,11 @@ Qed.
 Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a).
 Proof.
  intros a b Ha Hb. split; intros H.
- rewrite <- (sqrt_square b); trivial.
- now apply sqrt_le_mono.
- destruct (sqrt_spec a Ha) as (LE,LT).
- transitivity (√a)²; trivial.
- now apply mul_le_mono_nonneg.
+ - rewrite <- (sqrt_square b); trivial.
+   now apply sqrt_le_mono.
+ - destruct (sqrt_spec a Ha) as (LE,LT).
+   transitivity (√a)²; trivial.
+   now apply mul_le_mono_nonneg.
 Qed.
 
 (** When right side is a square, we have an equivalence for < *)
@@ -198,10 +198,10 @@ Qed.
 Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b).
 Proof.
  intros a b Ha Hb. split; intros H.
- destruct (sqrt_spec a Ha) as (LE,_).
- apply square_lt_simpl_nonneg; try order.
- rewrite <- (sqrt_square b Hb) in H.
- now apply sqrt_lt_cancel.
+ - destruct (sqrt_spec a Ha) as (LE,_).
+   apply square_lt_simpl_nonneg; try order.
+ - rewrite <- (sqrt_square b Hb) in H.
+   now apply sqrt_lt_cancel.
 Qed.
 
 (** Sqrt and basic constants *)
@@ -218,14 +218,14 @@ Qed.
 
 Lemma sqrt_2 : √2 == 1.
 Proof.
- apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'.
+  apply sqrt_unique' with 1. - nzsimpl; split; order'. - now nzsimpl'.
 Qed.
 
 Lemma sqrt_pos : forall a, 0 < √a <-> 0 < a.
 Proof.
- intros a. split; intros Ha. apply sqrt_lt_cancel. now rewrite sqrt_0.
- rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono.
- now rewrite one_succ, le_succ_l.
+  intros a. split; intros Ha. - apply sqrt_lt_cancel. now rewrite sqrt_0.
+  - rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono.
+    now rewrite one_succ, le_succ_l.
 Qed.
 
 Lemma sqrt_lt_lin : forall a, 1<a -> √a<a.
@@ -239,11 +239,11 @@ Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
 Proof.
  intros a Ha.
  destruct (le_gt_cases a 0) as [H|H].
- setoid_replace a with 0 by order. now rewrite sqrt_0.
- destruct (le_gt_cases a 1) as [H'|H'].
- rewrite <- le_succ_l, <- one_succ in H.
- setoid_replace a with 1 by order. now rewrite sqrt_1.
- now apply lt_le_incl, sqrt_lt_lin.
+ - setoid_replace a with 0 by order. now rewrite sqrt_0.
+ - destruct (le_gt_cases a 1) as [H'|H'].
+   + rewrite <- le_succ_l, <- one_succ in H.
+     setoid_replace a with 1 by order. now rewrite sqrt_1.
+   + now apply lt_le_incl, sqrt_lt_lin.
 Qed.
 
 (** Sqrt and multiplication. *)
@@ -255,28 +255,28 @@ Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
 Proof.
  intros a b.
  destruct (lt_ge_cases a 0) as [Ha|Ha].
- rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
- rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg.
- assert (Ha':=sqrt_nonneg a).
- assert (Hb':=sqrt_nonneg b).
- apply sqrt_le_square; try now apply mul_nonneg_nonneg.
- rewrite mul_shuffle1.
- apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg.
-  now apply sqrt_spec.
-  now apply sqrt_spec.
+ - rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg.
+ - destruct (lt_ge_cases b 0) as [Hb|Hb].
+   + rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg.
+   + assert (Ha':=sqrt_nonneg a).
+     assert (Hb':=sqrt_nonneg b).
+     apply sqrt_le_square; try now apply mul_nonneg_nonneg.
+     rewrite mul_shuffle1.
+     apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg.
+     * now apply sqrt_spec.
+     * now apply sqrt_spec.
 Qed.
 
 Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b).
 Proof.
  intros a b Ha Hb.
  apply sqrt_lt_square.
- now apply mul_nonneg_nonneg.
- apply mul_nonneg_nonneg.
- now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
- now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
- rewrite mul_shuffle1.
- apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec.
+ - now apply mul_nonneg_nonneg.
+ - apply mul_nonneg_nonneg.
+   + now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+   + now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+ - rewrite mul_shuffle1.
+   apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec.
 Qed.
 
 (** And we can't find better approximations in general.
@@ -296,73 +296,73 @@ Proof.
  intros a Ha.
  apply lt_succ_r.
  apply sqrt_lt_square.
- now apply le_le_succ_r.
- apply le_le_succ_r, le_le_succ_r, sqrt_nonneg.
- rewrite <- (add_1_l (S (√a))).
- apply lt_le_trans with (1²+(S (√a))²).
- rewrite mul_1_l, add_1_l, <- succ_lt_mono.
- now apply sqrt_spec.
- apply add_square_le. order'. apply le_le_succ_r, sqrt_nonneg.
+ - now apply le_le_succ_r.
+ - apply le_le_succ_r, le_le_succ_r, sqrt_nonneg.
+ - rewrite <- (add_1_l (S (√a))).
+   apply lt_le_trans with (1²+(S (√a))²).
+   + rewrite mul_1_l, add_1_l, <- succ_lt_mono.
+     now apply sqrt_spec.
+   + apply add_square_le. * order'. * apply le_le_succ_r, sqrt_nonneg.
 Qed.
 
 Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a.
 Proof.
  intros a Ha.
  destruct (le_gt_cases (√(S a)) (√a)) as [H|H].
- right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order.
- left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order.
+ - right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order.
+ - left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order.
 Qed.
 
 Lemma sqrt_eq_succ_iff_square : forall a, 0<=a ->
  (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²).
 Proof.
  intros a Ha. split.
- intros EQ. exists (S (√a)).
- split. apply lt_succ_r, sqrt_nonneg.
- generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l.
- assert (Ha' : 0 <= S a) by now apply le_le_succ_r.
- generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order.
- intros (b & Hb & H).
- rewrite H. rewrite sqrt_square; try order.
- symmetry.
- rewrite <- (lt_succ_pred 0 b Hb). f_equiv.
- rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H.
- now rewrite H, sqrt_pred_square.
- now apply mul_pos_pos.
+ - intros EQ. exists (S (√a)).
+   split. + apply lt_succ_r, sqrt_nonneg.
+   + generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l.
+     assert (Ha' : 0 <= S a) by now apply le_le_succ_r.
+     generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order.
+ - intros (b & Hb & H).
+   rewrite H. rewrite sqrt_square; try order.
+   symmetry.
+   rewrite <- (lt_succ_pred 0 b Hb). f_equiv.
+   rewrite <- (lt_succ_pred 0 b²) in H. + apply succ_inj in H.
+                                         now rewrite H, sqrt_pred_square.
+   + now apply mul_pos_pos.
 Qed.
 
 (** Sqrt and addition *)
 
 Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
 Proof.
- assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b).
-  intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl.
-  apply sqrt_le_mono.
-  rewrite <- (add_0_l b) at 2.
-  apply add_le_mono_r; order.
- intros a b.
- destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX.
- destruct (lt_ge_cases b 0) as [Hb|Hb].
-  rewrite (add_comm a), (add_comm (√a)); now apply AUX.
- assert (Ha':=sqrt_nonneg a).
- assert (Hb':=sqrt_nonneg b).
- rewrite <- lt_succ_r.
- apply sqrt_lt_square.
-  now apply add_nonneg_nonneg.
-  now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg.
- destruct (sqrt_spec a Ha) as (_,LTa).
- destruct (sqrt_spec b Hb) as (_,LTb).
- revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r.
- intros LTa LTb.
- assert (H:=add_le_mono _ _ _ _ LTa LTb).
- etransitivity; [eexact H|]. clear LTa LTb H.
- rewrite <- (add_assoc _ (√a) (√a)).
- rewrite <- (add_assoc _ (√b) (√b)).
- rewrite add_shuffle1.
- rewrite <- (add_assoc _ (√a + √b)).
- rewrite (add_shuffle1 (√a) (√b)).
- apply add_le_mono_r.
- now apply add_square_le.
+  assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b).
+  - intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl.
+    apply sqrt_le_mono.
+    rewrite <- (add_0_l b) at 2.
+    apply add_le_mono_r; order.
+  - intros a b.
+    destruct (lt_ge_cases a 0) as [Ha|Ha]. + now apply AUX.
+    + destruct (lt_ge_cases b 0) as [Hb|Hb].
+      * rewrite (add_comm a), (add_comm (√a)); now apply AUX.
+      * assert (Ha':=sqrt_nonneg a).
+        assert (Hb':=sqrt_nonneg b).
+        rewrite <- lt_succ_r.
+        apply sqrt_lt_square.
+        -- now apply add_nonneg_nonneg.
+        -- now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg.
+        -- destruct (sqrt_spec a Ha) as (_,LTa).
+           destruct (sqrt_spec b Hb) as (_,LTb).
+           revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r.
+           intros LTa LTb.
+           assert (H:=add_le_mono _ _ _ _ LTa LTb).
+           etransitivity; [eexact H|]. clear LTa LTb H.
+           rewrite <- (add_assoc _ (√a) (√a)).
+           rewrite <- (add_assoc _ (√b) (√b)).
+           rewrite add_shuffle1.
+           rewrite <- (add_assoc _ (√a + √b)).
+           rewrite (add_shuffle1 (√a) (√b)).
+           apply add_le_mono_r.
+           now apply add_square_le.
 Qed.
 
 (** convexity inequality for sqrt: sqrt of middle is above middle
@@ -374,12 +374,12 @@ Proof.
  assert (Ha':=sqrt_nonneg a).
  assert (Hb':=sqrt_nonneg b).
  apply sqrt_le_square.
-  apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg.
-  now apply add_nonneg_nonneg.
- transitivity (2*((√a)² + (√b)²)).
- now apply square_add_le.
- apply mul_le_mono_nonneg_l. order'.
- apply add_le_mono; now apply sqrt_spec.
+ - apply mul_nonneg_nonneg. + order'. + now apply add_nonneg_nonneg.
+ - now apply add_nonneg_nonneg.
+ - transitivity (2*((√a)² + (√b)²)).
+   + now apply square_add_le.
+   + apply mul_le_mono_nonneg_l. * order'.
+     * apply add_le_mono; now apply sqrt_spec.
 Qed.
 
 End NZSqrtProp.
@@ -430,8 +430,8 @@ Qed.
 Lemma sqrt_up_nonneg : forall a, 0<=√°a.
 Proof.
  intros. destruct (le_gt_cases a 0) as [Ha|Ha].
- now rewrite sqrt_up_eqn0.
- rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg.
+ - now rewrite sqrt_up_eqn0.
+ - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg.
 Qed.
 
 (** [sqrt_up] is a morphism *)
@@ -439,8 +439,8 @@ Qed.
 Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up.
 Proof.
  assert (Proper (eq==>eq==>Logic.eq) compare).
-  intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order.
- intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx.
+ - intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order.
+ - intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx.
 Qed.
 
 (** The spec of [sqrt_up] indeed determines it *)
@@ -463,9 +463,9 @@ Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a.
 Proof.
  intros a 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.
+ - 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.
 Qed.
 
 (** [sqrt_up] and successors of squares *)
@@ -500,10 +500,10 @@ Qed.
 Lemma le_sqrt_sqrt_up : forall a, √a <= √°a.
 Proof.
  intros a. unfold sqrt_up. case compare_spec; intros H.
- rewrite <- H, sqrt_0. order.
- rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le.
- apply lt_succ_r. now rewrite (lt_succ_pred 0 a H).
- now rewrite sqrt_neg.
+ - rewrite <- H, sqrt_0. order.
+ - rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le.
+   apply lt_succ_r. now rewrite (lt_succ_pred 0 a H).
+ - now rewrite sqrt_neg.
 Qed.
 
 Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a).
@@ -517,21 +517,21 @@ Qed.
 Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)².
 Proof.
  intros a H. split.
- now apply sqrt_spec.
- le_elim H.
- now apply sqrt_up_spec.
- now rewrite <-H, sqrt_up_0, mul_0_l.
+ - now apply sqrt_spec.
+ - le_elim H.
+   + now apply sqrt_up_spec.
+   + now rewrite <-H, sqrt_up_0, mul_0_l.
 Qed.
 
 Lemma sqrt_sqrt_up_exact :
  forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²).
 Proof.
  intros a Ha.
- split. intros. exists √a.
-  split. apply sqrt_nonneg.
-  generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order.
- intros (b & Hb & Hb'). rewrite Hb'.
- now rewrite sqrt_square, sqrt_up_square.
+ split. - intros. exists √a.
+          split. + apply sqrt_nonneg.
+          + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order.
+ - intros (b & Hb & Hb'). rewrite Hb'.
+   now rewrite sqrt_square, sqrt_up_square.
 Qed.
 
 (** [sqrt_up] is a monotone function (but not a strict one) *)
@@ -540,9 +540,9 @@ Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b.
 Proof.
  intros a b H.
  destruct (le_gt_cases a 0) as [Ha|Ha].
- rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg.
- rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono.
- apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order.
+ - rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg.
+ - rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono.
+   apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order.
 Qed.
 
 (** No reverse result for <=, consider for instance √°3 <= √°2 *)
@@ -551,10 +551,10 @@ Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b.
 Proof.
  intros a b H.
  destruct (le_gt_cases b 0) as [Hb|Hb].
- rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order.
- destruct (le_gt_cases a 0) as [Ha|Ha]; [order|].
- rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono.
- apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn.
+ - rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order.
+ - destruct (le_gt_cases a 0) as [Ha|Ha]; [order|].
+   rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono.
+   apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn.
 Qed.
 
 (** When left side is a square, we have an equivalence for < *)
@@ -562,10 +562,10 @@ Qed.
 Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a).
 Proof.
  intros a b Ha Hb. split; intros H.
- destruct (sqrt_up_spec a) as (LE,LT).
- apply le_lt_trans with b²; trivial using square_nonneg.
- apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg.
- apply sqrt_up_lt_cancel. now rewrite sqrt_up_square.
+ - destruct (sqrt_up_spec a) as (LE,LT).
+   + apply le_lt_trans with b²; trivial using square_nonneg.
+   + apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg.
+ - apply sqrt_up_lt_cancel. now rewrite sqrt_up_square.
 Qed.
 
 (** When right side is a square, we have an equivalence for <= *)
@@ -573,17 +573,17 @@ Qed.
 Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b).
 Proof.
  intros a b Ha Hb. split; intros H.
- rewrite <- (sqrt_up_square b Hb).
- now apply sqrt_up_le_mono.
- apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg].
- transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec.
+ - rewrite <- (sqrt_up_square b Hb).
+   now apply sqrt_up_le_mono.
+ - apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg].
+   transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec.
 Qed.
 
 Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a.
 Proof.
- intros a. split; intros Ha. apply sqrt_up_lt_cancel. now rewrite sqrt_up_0.
- rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono.
- now rewrite one_succ, le_succ_l.
+  intros a. split; intros Ha. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_0.
+  - rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono.
+    now rewrite one_succ, le_succ_l.
 Qed.
 
 Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a.
@@ -599,11 +599,11 @@ Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a.
 Proof.
  intros a 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).
- rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r.
- now rewrite <- Ha, sqrt_up_0.
+ - 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).
+   + rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r.
+ - now rewrite <- Ha, sqrt_up_0.
 Qed.
 
 (** [sqrt_up] and multiplication. *)
@@ -615,23 +615,23 @@ Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √
 Proof.
  intros a b Ha Hb.
  apply sqrt_up_le_square.
- now apply mul_nonneg_nonneg.
- apply mul_nonneg_nonneg; apply sqrt_up_nonneg.
- rewrite mul_shuffle1.
- apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec.
+ - now apply mul_nonneg_nonneg.
+ - apply mul_nonneg_nonneg; apply sqrt_up_nonneg.
+ - rewrite mul_shuffle1.
+   apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec.
 Qed.
 
 Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b).
 Proof.
  intros a b Ha Hb.
  apply sqrt_up_lt_square.
- apply mul_nonneg_nonneg; order.
- apply mul_nonneg_nonneg; apply lt_succ_r.
- rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
- rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
- rewrite mul_shuffle1.
- apply mul_lt_mono_nonneg; trivial using square_nonneg;
-  now apply sqrt_up_spec.
+ - apply mul_nonneg_nonneg; order.
+ - apply mul_nonneg_nonneg; apply lt_succ_r.
+   + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
+   + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
+ - rewrite mul_shuffle1.
+   apply mul_lt_mono_nonneg; trivial using square_nonneg;
+     now apply sqrt_up_spec.
 Qed.
 
 (** And we can't find better approximations in general.
@@ -650,37 +650,37 @@ Lemma sqrt_up_succ_le : forall a, 0<=a -> √°(S a) <= S (√°a).
 Proof.
  intros a Ha.
  apply sqrt_up_le_square.
- now apply le_le_succ_r.
- apply le_le_succ_r, sqrt_up_nonneg.
- rewrite <- (add_1_l (√°a)).
- apply le_trans with (1²+(√°a)²).
- rewrite mul_1_l, add_1_l, <- succ_le_mono.
- now apply sqrt_sqrt_up_spec.
- apply add_square_le. order'. apply sqrt_up_nonneg.
+ - now apply le_le_succ_r.
+ - apply le_le_succ_r, sqrt_up_nonneg.
+ - rewrite <- (add_1_l (√°a)).
+   apply le_trans with (1²+(√°a)²).
+   + rewrite mul_1_l, add_1_l, <- succ_le_mono.
+     now apply sqrt_sqrt_up_spec.
+   + apply add_square_le. * order'. * apply sqrt_up_nonneg.
 Qed.
 
 Lemma sqrt_up_succ_or : forall a, 0<=a -> √°(S a) == S (√°a) \/ √°(S a) == √°a.
 Proof.
  intros a Ha.
  destruct (le_gt_cases (√°(S a)) (√°a)) as [H|H].
- right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order.
- left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order.
+ - right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order.
+ - left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order.
 Qed.
 
 Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a ->
  (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²).
 Proof.
  intros a Ha. split.
- intros EQ.
- 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').
- generalize (proj1 (sqrt_up_spec (S a) Ha')).
- rewrite EQ, pred_succ, lt_succ_r. order.
- exists 0. nzsimpl. now split.
- intros (b & Hb & H).
- now rewrite H, sqrt_up_succ_square, sqrt_up_square.
+ - intros EQ.
+   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').
+       generalize (proj1 (sqrt_up_spec (S a) Ha')).
+       rewrite EQ, pred_succ, lt_succ_r. order.
+   + exists 0. nzsimpl. now split.
+ - intros (b & Hb & H).
+   now rewrite H, sqrt_up_succ_square, sqrt_up_square.
 Qed.
 
 (** [sqrt_up] and addition *)
@@ -688,21 +688,21 @@ Qed.
 Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b.
 Proof.
  assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b).
-  intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl.
-  apply sqrt_up_le_mono.
-  rewrite <- (add_0_l b) at 2.
-  apply add_le_mono_r; order.
- intros a b.
- destruct (le_gt_cases a 0) as [Ha|Ha]. now apply AUX.
- destruct (le_gt_cases b 0) as [Hb|Hb].
-  rewrite (add_comm a), (add_comm (√°a)); now apply AUX.
- rewrite 2 sqrt_up_eqn; trivial.
- nzsimpl. rewrite <- succ_le_mono.
- transitivity (√(P a) + √b).
- rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le.
- apply add_le_mono_l.
- apply le_sqrt_sqrt_up.
- now apply add_pos_pos.
+ - intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl.
+   apply sqrt_up_le_mono.
+   rewrite <- (add_0_l b) at 2.
+   apply add_le_mono_r; order.
+ - intros a b.
+   destruct (le_gt_cases a 0) as [Ha|Ha]. + now apply AUX.
+   + destruct (le_gt_cases b 0) as [Hb|Hb].
+     * rewrite (add_comm a), (add_comm (√°a)); now apply AUX.
+     * rewrite 2 sqrt_up_eqn; trivial.
+       -- nzsimpl. rewrite <- succ_le_mono.
+          transitivity (√(P a) + √b).
+          ++ rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le.
+          ++ apply add_le_mono_l.
+             apply le_sqrt_sqrt_up.
+       -- now apply add_pos_pos.
 Qed.
 
 (** Convexity-like inequality for [sqrt_up]: [sqrt_up] of middle is above middle
@@ -712,25 +712,24 @@ 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.
- le_elim Ha.
- le_elim Hb.
- rewrite 3 sqrt_up_eqn; trivial.
- nzsimpl. rewrite <- 2 succ_le_mono.
- etransitivity; [eapply add_sqrt_le|].
- apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha).
- apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb).
- apply sqrt_le_mono.
- apply lt_succ_r. rewrite (lt_succ_pred 0).
- apply mul_lt_mono_pos_l. order'.
- apply add_lt_mono.
- apply le_succ_l. now rewrite (lt_succ_pred 0).
- apply le_succ_l. now rewrite (lt_succ_pred 0).
- apply mul_pos_pos. order'. now apply add_pos_pos.
- apply mul_pos_pos. order'. now apply add_pos_pos.
- rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono.
- rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'.
- rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono.
- rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'.
+ le_elim Ha;[le_elim Hb|].
+ - rewrite 3 sqrt_up_eqn; trivial.
+   + nzsimpl. rewrite <- 2 succ_le_mono.
+     etransitivity; [eapply add_sqrt_le|].
+     * apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha).
+     * apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb).
+     * apply sqrt_le_mono.
+       apply lt_succ_r. rewrite (lt_succ_pred 0).
+       -- apply mul_lt_mono_pos_l. ++ order'.
+          ++ apply add_lt_mono.
+             ** apply le_succ_l. now rewrite (lt_succ_pred 0).
+             ** apply le_succ_l. now rewrite (lt_succ_pred 0).
+       -- apply mul_pos_pos. ++ order'. ++ now apply add_pos_pos.
+   + apply mul_pos_pos. * order'. * now apply add_pos_pos.
+ - rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono.
+   rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'.
+ - rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono.
+   rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'.
 Qed.
 
 End NZSqrtUpProp.