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

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

48 files changed, 1759 insertions, 1696 deletions

diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index 106a79e8c9..59a1b8da43 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -67,8 +67,8 @@ Section Bool_eq_dec.
   Proof.
     intros x y; case (exists_beq_eq x y).
     intros b; case b; intro H.
-      left; apply beq_eq; assumption.
-      right; apply beq_false_not_eq; assumption.
+    - left; apply beq_eq; assumption.
+    - right; apply beq_false_not_eq; assumption.
   Defined.
 
 End Bool_eq_dec.
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 6f99ea1da7..32ed7fe78d 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -45,6 +45,6 @@ Qed.
 
 Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
 destruct b; intro H.
-left; inversion H; auto with bool.
-right; inversion H; auto with bool.
+- left; inversion H; auto with bool.
+- right; inversion H; auto with bool.
 Qed.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 97510578ae..f9ca1bed29 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -164,7 +164,11 @@ Section Relations.
 
   Lemma pointwise_pointwise {B} (R : crelation B) :
     relation_equivalence (pointwise_relation R) (@eq A ==> R).
-  Proof. intros. split. simpl_crelation. firstorder. Qed.
+  Proof.
+    intros. split.
+    - simpl_crelation.
+    - firstorder.
+  Qed.
   
   (** Subcrelations induce a morphism on the identity. *)
   
@@ -265,8 +269,8 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     assert(R x0 x0).
-    transitivity y0... symmetry...
-    transitivity (y x0)...
+    - transitivity y0... symmetry...
+    - transitivity (y x0)...
   Qed.
 
   Unset Strict Universe Declaration.
@@ -339,10 +343,11 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
-    split. intros ; transitivity x0...
-    intros.
-    transitivity y...
-    symmetry...
+    split.
+    - intros ; transitivity x0...
+    - intros.
+      transitivity y...
+      symmetry...
   Qed.
 
   (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
@@ -364,9 +369,9 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     split ; intros.
-    transitivity x0... transitivity x... symmetry...
+    - transitivity x0... transitivity x... symmetry...
 
-    transitivity y... transitivity y0... symmetry...
+    - transitivity y... transitivity y0... symmetry...
   Qed.
 
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
@@ -397,8 +402,8 @@ Section GenericInstances.
     intros A B R R' HRR' S S' HSS' f g. 
     unfold respectful , relation_equivalence in *; simpl in *.
     split ; intros H x y Hxy.
-    apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). 
-    apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). 
+    - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)).
+    - apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)).
   Qed.
 
   (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -500,8 +505,8 @@ Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper
 Proof.
   intros A R R' HRR' x y <-. red in HRR'.
   split ; red ; intros. 
-  now apply (fst (HRR' _ _)). 
-  now apply (snd (HRR' _ _)).
+  - now apply (fst (HRR' _ _)).
+  - now apply (snd (HRR' _ _)).
 Qed.
 
 Ltac proper_reflexive :=
@@ -636,9 +641,9 @@ intros.
 apply proper_sym_arrow_iffT_2; auto with *.
 intros x x' Hx y y' Hy Hr.
 transitivity x.
-generalize (partial_order_equivalence x x'); compute; intuition.
-transitivity y; auto.
-generalize (partial_order_equivalence y y'); compute; intuition.
+- generalize (partial_order_equivalence x x'); compute; intuition.
+- transitivity y; auto.
+  generalize (partial_order_equivalence y y'); compute; intuition.
 Qed.
 
 (** From a [PartialOrder] to the corresponding [StrictOrder]:
@@ -649,13 +654,13 @@ Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
   StrictOrder (relation_conjunction R (complement eqA)).
 Proof.
 split; compute.
-intros x (_,Hx). apply Hx, Equivalence_Reflexive.
-intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
-apply PreOrder_Transitive with y; assumption.
-intro Hxz.
-apply Hxy'.
-apply partial_order_antisym; auto.
-rewrite Hxz. auto.
+- intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+- intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+  + apply PreOrder_Transitive with y; assumption.
+  + intro Hxz.
+    apply Hxy'.
+    apply partial_order_antisym; auto.
+    rewrite Hxz. auto.
 Qed.
 
 (** From a [StrictOrder] to the corresponding [PartialOrder]:
@@ -667,12 +672,12 @@ Lemma StrictOrder_PreOrder
  PreOrder (relation_disjunction R eqA).
 Proof.
 split.
-intros x. right. reflexivity.
-intros x y z [Hxy|Hxy] [Hyz|Hyz].
-left. transitivity y; auto.
-left. rewrite <- Hyz; auto.
-left. rewrite Hxy; auto.
-right. transitivity y; auto.
+- intros x. right. reflexivity.
+- intros x y z [Hxy|Hxy] [Hyz|Hyz].
+  + left. transitivity y; auto.
+  + left. rewrite <- Hyz; auto.
+  + left. rewrite Hxy; auto.
+  + right. transitivity y; auto.
 Qed.
 
 Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index bb873588b1..c014ecc7ab 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -315,9 +315,11 @@ Section Binary.
 
   Global Instance relation_equivalence_equivalence :
     Equivalence relation_equivalence.
-  Proof. split; red; unfold relation_equivalence, iffT. firstorder. 
-    firstorder. 
-    intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
+  Proof.
+    split; red; unfold relation_equivalence, iffT.
+    - firstorder.
+    - firstorder.
+    - intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
   Qed.
     
   Global Instance relation_implication_preorder : PreOrder (@subrelation A).
@@ -342,8 +344,11 @@ Section Binary.
   Qed.
 
   Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
-  Proof. unfold flip; constructor; unfold flip. intros. apply H. apply symmetry. apply X.
-         unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed.
+  Proof.
+    unfold flip; constructor; unfold flip.
+    - intros. apply H. apply symmetry. apply X.
+    - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption.
+  Qed.
 End Binary.
 
 Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 001b7dfdfd..a4fa537128 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -260,8 +260,8 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     assert(R x0 x0).
-    transitivity y0... symmetry...
-    transitivity (y x0)... 
+    - transitivity y0... symmetry...
+    - transitivity (y x0)...
   Qed.
 
   (** The complement of a relation conserves its proper elements. *)
@@ -344,10 +344,11 @@ Section GenericInstances.
 
   Next Obligation.
   Proof with auto.
-    split. intros ; transitivity x0...
-    intros.
-    transitivity y...
-    symmetry...
+    split.
+    - intros ; transitivity x0...
+    - intros.
+      transitivity y...
+      symmetry...
   Qed.
 
   (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
@@ -369,9 +370,9 @@ Section GenericInstances.
   Next Obligation.
   Proof with auto.
     split ; intros.
-    transitivity x0... transitivity x... symmetry...
+    - transitivity x0... transitivity x... symmetry...
 
-    transitivity y... transitivity y0... symmetry...
+    - transitivity y... transitivity y0... symmetry...
   Qed.
 
   Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
@@ -403,15 +404,15 @@ Section GenericInstances.
     unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
     split ; intros.
     
-    rewrite <- H0.
-    apply H1.
-    rewrite H.
-    assumption.
-    
-    rewrite H0.
-    apply H1.
-    rewrite <- H.
-    assumption.
+    - rewrite <- H0.
+      apply H1.
+      rewrite H.
+      assumption.
+
+    - rewrite H0.
+      apply H1.
+      rewrite <- H.
+      assumption.
   Qed.
 
   (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -514,10 +515,10 @@ Proof.
   simpl_relation.
   reduce in H.
   split ; red ; intros.
-  setoid_rewrite <- H.
-  apply H0.
-  setoid_rewrite H.
-  apply H0.
+  - setoid_rewrite <- H.
+    apply H0.
+  - setoid_rewrite H.
+    apply H0.
 Qed.
 
 Ltac proper_reflexive :=
@@ -574,8 +575,8 @@ Proof.
   unfold relation_equivalence in *. 
   unfold predicate_equivalence in *. simpl in *.
   unfold respectful. unfold flip in *. firstorder.
-  apply NB. apply H. apply NA. apply H0.
-  apply NB. apply H. apply NA. apply H0.
+  - apply NB. apply H. apply NA. apply H0.
+  - apply NB. apply H. apply NA. apply H0.
 Qed.
 
 Ltac normalizes :=
@@ -642,9 +643,9 @@ intros.
 apply proper_sym_impl_iff_2; auto with *.
 intros x x' Hx y y' Hy Hr.
 transitivity x.
-generalize (partial_order_equivalence x x'); compute; intuition.
-transitivity y; auto.
-generalize (partial_order_equivalence y y'); compute; intuition.
+- generalize (partial_order_equivalence x x'); compute; intuition.
+- transitivity y; auto.
+  generalize (partial_order_equivalence y y'); compute; intuition.
 Qed.
 
 (** From a [PartialOrder] to the corresponding [StrictOrder]:
@@ -655,13 +656,13 @@ Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
   StrictOrder (relation_conjunction R (complement eqA)).
 Proof.
 split; compute.
-intros x (_,Hx). apply Hx, Equivalence_Reflexive.
-intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
-apply PreOrder_Transitive with y; assumption.
-intro Hxz.
-apply Hxy'.
-apply partial_order_antisym; auto.
-rewrite Hxz; auto.
+- intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+- intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+  + apply PreOrder_Transitive with y; assumption.
+  + intro Hxz.
+    apply Hxy'.
+    apply partial_order_antisym; auto.
+    rewrite Hxz; auto.
 Qed.
 
 
@@ -674,12 +675,12 @@ Lemma StrictOrder_PreOrder
  PreOrder (relation_disjunction R eqA).
 Proof.
 split.
-intros x. right. reflexivity.
-intros x y z [Hxy|Hxy] [Hyz|Hyz].
-left. transitivity y; auto.
-left. rewrite <- Hyz; auto.
-left. rewrite Hxy; auto.
-right. transitivity y; auto.
+- intros x. right. reflexivity.
+- intros x y z [Hxy|Hxy] [Hyz|Hyz].
+  + left. transitivity y; auto.
+  + left. rewrite <- Hyz; auto.
+  + left. rewrite Hxy; auto.
+  + right. transitivity y; auto.
 Qed.
 
 Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 8881fda577..efb85aa341 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -85,10 +85,12 @@ Qed.
 Instance Acc_rel_morphism {A:Type} :
  Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A).
 Proof.
- apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry.
- intros R R' EQ a a' Ha WF. subst a'.
- induction WF as [x _ WF']. constructor.
- intros y Ryx. now apply WF', EQ.
+  apply proper_sym_impl_iff_2.
+  - red; now symmetry.
+  - red; now symmetry.
+  - intros R R' EQ a a' Ha WF. subst a'.
+    induction WF as [x _ WF']. constructor.
+    intros y Ryx. now apply WF', EQ.
 Qed.
 
 (** Equivalent relations are simultaneously well-founded or not *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 6e2ff49536..440b317573 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -407,9 +407,10 @@ Program Instance predicate_equivalence_equivalence :
   Qed.
   Next Obligation.
     fold pointwise_lifting.
-    induction l. firstorder.
-    intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
-    firstorder.
+    induction l.
+    - firstorder.
+    - intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
+      firstorder.
   Qed.
 
 Program Instance predicate_implication_preorder :
@@ -418,9 +419,10 @@ Program Instance predicate_implication_preorder :
     induction l ; firstorder.
   Qed.
   Next Obligation.
-    induction l. firstorder.
-    unfold predicate_implication in *. simpl in *.
-    intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+    induction l.
+    - firstorder.
+    - unfold predicate_implication in *. simpl in *.
+      intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
   Qed.
 
 (** We define the various operations which define the algebra on binary relations,
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 1db0a8e1b5..b607be4f94 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -383,6 +383,11 @@ Section Logic_lemmas.
 
     Register eq_trans as core.eq.trans.
 
+    Theorem eq_trans_r : x = y -> z = y -> x = z.
+    Proof.
+      destruct 2; trivial.
+    Defined.
+
     Theorem f_equal : x = y -> f x = f y.
     Proof.
       destruct 1; trivial.
@@ -695,8 +700,8 @@ Proof.
   - intros (x,(Hx,Huni)); split.
     + exists x; assumption.
     + intros x' x'' Hx' Hx''; transitivity x.
-      symmetry; auto.
-      auto.
+      * symmetry; auto.
+      * auto.
 Qed.
 
 Lemma forall_exists_unique_domain_coincide :
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index cfba2bae69..e5d63c547d 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -765,8 +765,9 @@ Section Dependent_choice_lemmas.
     intros H x0.
     set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
     exists f.
-    split. reflexivity.
-    induction n; simpl; apply proj2_sig.
+    split.
+    - reflexivity.
+    - induction n; simpl; apply proj2_sig.
   Defined.
 
 End Dependent_choice_lemmas.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 8df533e743..af4632161e 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -202,13 +202,17 @@ Set Implicit Arguments.
 Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
   C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
 Proof.
-intros; destruct decide. apply H0. contradiction.
+  intros; destruct decide.
+  - apply H0.
+  - contradiction.
 Qed.
 
 Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),
   ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
 Proof.
-intros; destruct decide. contradiction. apply H0.
+  intros; destruct decide.
+  - contradiction.
+  - apply H0.
 Qed.
 
 Tactic Notation "decide" constr(lemma) "with" constr(H) :=
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index d93816e9ff..419a0be49c 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -118,16 +118,16 @@ intros n; unfold dmemo_get, dmemo_list.
 rewrite (memo_get_correct memo_val mf n); simpl.
 case (is_eq n n); simpl; auto; intros e.
 assert (e = eq_refl n).
- apply eq_proofs_unicity.
- induction x as [| x Hx]; destruct y as [| y].
- left; auto.
- right; intros HH; discriminate HH.
- right; intros HH; discriminate HH.
- case (Hx y).
-   intros HH; left; case HH; auto.
- intros HH; right; intros HH1; case HH.
- injection HH1; auto.
-rewrite H; auto.
+- apply eq_proofs_unicity.
+  induction x as [| x Hx]; destruct y as [| y].
+  + left; auto.
+  + right; intros HH; discriminate HH.
+  + right; intros HH; discriminate HH.
+  + case (Hx y).
+    * intros HH; left; case HH; auto.
+    * intros HH; right; intros HH1; case HH.
+      injection HH1; auto.
+- rewrite H; auto.
 Qed.
 
 (** Finally, a version with both dependency and iterator *)
@@ -145,19 +145,19 @@ Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n.
 Proof.
 intros n; unfold dmemo_get, dimemo_list.
 rewrite (imemo_get_correct memo_val mf mg); simpl.
-case (is_eq n n); simpl; auto; intros e.
-assert (e = eq_refl n).
- apply eq_proofs_unicity.
- induction x as [| x Hx]; destruct y as [| y].
- left; auto.
- right; intros HH; discriminate HH.
- right; intros HH; discriminate HH.
- case (Hx y).
-   intros HH; left; case HH; auto.
- intros HH; right; intros HH1; case HH.
- injection HH1; auto.
-rewrite H; auto.
-intros n1; unfold mf; rewrite Hg_correct; auto.
+- case (is_eq n n); simpl; auto; intros e.
+  assert (e = eq_refl n).
+  + apply eq_proofs_unicity.
+    induction x as [| x Hx]; destruct y as [| y].
+    * left; auto.
+    * right; intros HH; discriminate HH.
+    * right; intros HH; discriminate HH.
+    * case (Hx y).
+      -- intros HH; left; case HH; auto.
+      -- intros HH; right; intros HH1; case HH.
+         injection HH1; auto.
+  + rewrite H; auto.
+- intros n1; unfold mf; rewrite Hg_correct; auto.
 Qed.
 
 End DependentMemoFunction.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index a03799959e..4503b3b643 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -92,20 +92,20 @@ Qed.
 
 Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
 coinduction Eq_sym.
-case H; intros; symmetry ; assumption.
-case H; intros; assumption.
++ case H; intros; symmetry ; assumption.
++ case H; intros; assumption.
 Qed.
 
 
 Theorem trans_EqSt :
  forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.
 coinduction Eq_trans.
-transitivity (hd s2).
-case H; intros; assumption.
-case H0; intros; assumption.
-apply (Eq_trans (tl s1) (tl s2) (tl s3)).
-case H; trivial with datatypes.
-case H0; trivial with datatypes.
+- transitivity (hd s2).
+  + case H; intros; assumption.
+  + case H0; intros; assumption.
+- apply (Eq_trans (tl s1) (tl s2) (tl s3)).
+  + case H; trivial with datatypes.
+  + case H0; trivial with datatypes.
 Qed.
 
 (** The definition given is equivalent to require the elements at each
@@ -114,20 +114,20 @@ Qed.
 Theorem eqst_ntheq :
  forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
 unfold Str_nth; simple induction n.
-intros s1 s2 H; case H; trivial with datatypes.
-intros m hypind.
-simpl.
-intros s1 s2 H.
-apply hypind.
-case H; trivial with datatypes.
+- intros s1 s2 H; case H; trivial with datatypes.
+- intros m hypind.
+  simpl.
+  intros s1 s2 H.
+  apply hypind.
+  case H; trivial with datatypes.
 Qed.
 
 Theorem ntheq_eqst :
  forall s1 s2:Stream,
    (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.
 coinduction Equiv2.
-apply (H 0).
-intros n; apply (H (S n)).
+- apply (H 0).
+- intros n; apply (H (S n)).
 Qed.
 
 Section Stream_Properties.
@@ -150,11 +150,11 @@ CoInductive ForAll (x: Stream) : Prop :=
 Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x).
 Proof.
 induction m.
- tauto.
-intros x [_ H].
-simpl.
-apply IHm.
-assumption.
+- tauto.
+- intros x [_ H].
+  simpl.
+  apply IHm.
+  assumption.
 Qed.
 
 Section Co_Induction_ForAll.
@@ -179,10 +179,10 @@ CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).
 Lemma Str_nth_tl_map : forall n s, Str_nth_tl n (map s)= map (Str_nth_tl n s).
 Proof.
 induction n.
-reflexivity.
-simpl.
-intros s.
-apply IHn.
+- reflexivity.
+- simpl.
+  intros s.
+  apply IHn.
 Qed.
 
 Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s).
@@ -228,11 +228,11 @@ Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B),
  Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).
 Proof.
 induction n.
-reflexivity.
-intros [x xs] [y ys].
-unfold Str_nth in *.
-simpl in *.
-apply IHn.
+- reflexivity.
+- intros [x xs] [y ys].
+  unfold Str_nth in *.
+  simpl in *.
+  apply IHn.
 Qed.
 
 Lemma Str_nth_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth n (zipWith a
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index ed4d69ab02..86894cd1f2 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -88,8 +88,8 @@ Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
 Proof.
 intros A B.
 destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
-  exists f0 g0; trivial.
-  exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
+- exists f0 g0; trivial.
+- exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
     destruct hf; auto.
 Qed.
 
@@ -130,9 +130,9 @@ Proof.
 unfold R at 1.
 unfold g.
 rewrite AC.
-trivial.
-exists (fun x:pow U => x) (fun x:pow U => x).
-trivial.
+- trivial.
+- exists (fun x:pow U => x) (fun x:pow U => x).
+  trivial.
 Qed.
 
 
@@ -141,11 +141,11 @@ Proof.
 generalize not_has_fixpoint.
 unfold Not_b.
 apply AC_IF.
-intros is_true is_false.
-elim is_true; elim is_false; trivial.
+- intros is_true is_false.
+  elim is_true; elim is_false; trivial.
 
-intros not_true is_true.
-elim not_true; trivial.
+- intros not_true is_true.
+  elim not_true; trivial.
 Qed.
 
 
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 8e59941f37..b930388d13 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -372,8 +372,7 @@ Proof.
   rewrite (UIP_refl y).
   intros z.
   assert (UIP:forall y' y'' : x = x, y' = y'').
-  { intros. apply eq_trans with (eq_refl x). apply UIP_refl.
-    symmetry. apply UIP_refl. }
+  { intros. apply eq_trans_r with (eq_refl x); apply UIP_refl. }
   transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
                          (eq_sym (UIP (eq_refl x) (eq_refl x)))).
   - destruct z. destruct (UIP _ _). reflexivity.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 4e8b48af9f..3babc9437b 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -66,9 +66,9 @@ Section EqdepDec.
     intros.
     unfold nu.
     destruct (eq_dec y) as [Heq|Hneq].
-    reflexivity.
+    - reflexivity.
 
-    case Hneq; trivial.
+    - case Hneq; trivial.
   Qed.
 
 
@@ -118,15 +118,15 @@ Section EqdepDec.
   Proof.
     intros.
     cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
-    simpl.
-    destruct (eq_dec x) as [Heq|Hneq].
-    elim Heq using K_dec_on; trivial.
+    - simpl.
+      destruct (eq_dec x) as [Heq|Hneq].
+      + elim Heq using K_dec_on; trivial.
 
-    intros.
-    case Hneq; trivial.
+      + intros.
+        case Hneq; trivial.
 
-    case H.
-    reflexivity.
+    - case H.
+      reflexivity.
   Qed.
 
 End EqdepDec.
@@ -163,8 +163,8 @@ Theorem K_dec_type :
 Proof.
   intros A eq_dec x P H p.
   elim p using K_dec; intros.
-  case (eq_dec x0 y); [left|right]; assumption.
-  trivial.
+  - case (eq_dec x0 y); [left|right]; assumption.
+  - trivial.
 Qed.
 
 Theorem K_dec_set :
@@ -260,8 +260,8 @@ Module DecidableEqDep (M:DecidableType).
   Proof.
     intros.
     apply inj_right_pair with (A:=U).
-    intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
-    assumption.
+    - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
+    - assumption.
   Qed.
 
 End DecidableEqDep.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 3914f44a2c..11897b6cb1 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -135,10 +135,10 @@ Proof.
 exists bool. exists (fun _ => True). exists true. exists false.
 exists I. exists I.
 split.
-trivial.
-intro H.
-assert (true=false) by (destruct H; reflexivity).
-discriminate.
+- trivial.
+- intro H.
+  assert (true=false) by (destruct H; reflexivity).
+  discriminate.
 Qed.
 
 (** However, when the dependencies are equal, [JMeq (P p) x (P q) y]
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.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 1c89b6c3b1..ae366204ac 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -73,10 +73,10 @@ Proof.
   simpl.
   split ; intros ; subst.
 
-  inversion H.
-  reflexivity.
+  - inversion H.
+    reflexivity.
 
-  pi.
+  - pi.
 Qed.
 
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index f9d23e3cf6..092c1d6f48 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -97,15 +97,15 @@ Section Measure_well_founded.
   Proof with auto.
     unfold well_founded.
     cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
-      intros.
+    + intros.
       apply (H (m a))...
-    apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
-    intros.
-    apply Acc_intro.
-    intros.
-    unfold MR in H1.
-    rewrite H0 in H1.
-    apply (H (m y))...
+    + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
+      intros.
+      apply Acc_intro.
+      intros.
+      unfold MR in H1.
+      rewrite H0 in H1.
+      apply (H (m y))...
   Defined.
 
 End Measure_well_founded.
@@ -245,8 +245,8 @@ Module WfExtensionality.
     intros ; apply Fix_eq ; auto.
     intros.
     assert(f = g).
-    extensionality y ; apply H.
-    rewrite H0 ; auto.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
   Qed.
 
   (** Tactic to unfold once a definition based on [Fix_sub]. *)
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index e82a673445..0a60d96afc 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -45,9 +45,8 @@ Section Properties.
     Lemma clos_rt_is_preorder : preorder R*.
     Proof.
       apply Build_preorder.
-      exact (rt_refl A R).
-
-      exact (rt_trans A R).
+      - exact (rt_refl A R).
+      - exact (rt_trans A R).
     Qed.
 
     (** Idempotency of the reflexive-transitive closure operator *)
@@ -82,8 +81,8 @@ Section Properties.
       inclusion (clos_refl R) (clos_refl_trans R).
     Proof.
       induction 1 as [? ?| ].
-      constructor; auto.
-      constructor 2.
+      - constructor; auto.
+      - constructor 2.
     Qed.
 
     Lemma clos_rt_t : forall x y z,
@@ -100,9 +99,9 @@ Section Properties.
     Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R).
     Proof.
       apply Build_equivalence.
-      exact (rst_refl A R).
-      exact (rst_trans A R).
-      exact (rst_sym A R).
+      - exact (rst_refl A R).
+      - exact (rst_trans A R).
+      - exact (rst_sym A R).
     Qed.
 
     (** Idempotency of the reflexive-symmetric-transitive closure operator *)
@@ -130,18 +129,18 @@ Section Properties.
     Lemma clos_t1n_trans : forall x y, clos_trans_1n R x y -> clos_trans R x y.
     Proof.
      induction 1.
-     left; assumption.
-     right with y; auto.
-     left; auto.
+     - left; assumption.
+     - right with y; auto.
+       left; auto.
     Qed.
 
     Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y.
     Proof.
       induction 1.
-      left; assumption.
-      generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1.
-      right with y; auto.
-      right with y; auto.
+      - left; assumption.
+      - generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1.
+        + right with y; auto.
+        + right with y; auto.
       eapply IHIHclos_trans1; auto.
       apply clos_t1n_trans; auto.
     Qed.
@@ -150,8 +149,8 @@ Section Properties.
         clos_trans R x y <-> clos_trans_1n R x y.
     Proof.
       split.
-      apply clos_trans_t1n.
-      apply clos_t1n_trans.
+      - apply clos_trans_t1n.
+      - apply clos_t1n_trans.
     Qed.
 
     (** Direct transitive closure vs right-step extension *)
@@ -159,29 +158,29 @@ Section Properties.
     Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y.
     Proof.
       induction 1.
-      left; assumption.
-      right with y; auto.
-      left; assumption.
+      - left; assumption.
+      - right with y; auto.
+        left; assumption.
     Qed.
 
     Lemma clos_trans_tn1 :  forall x y, clos_trans R x y -> clos_trans_n1 R x y.
     Proof.
       induction 1.
-      left; assumption.
-      elim IHclos_trans2.
-      intro y0; right with y.
-      auto.
-      auto.
-      intros.
-      right with y0; auto.
+      - left; assumption.
+      - elim IHclos_trans2.
+        + intro y0; right with y.
+          *  auto.
+          * auto.
+        + intros.
+          right with y0; auto.
     Qed.
 
     Lemma clos_trans_tn1_iff : forall x y,
         clos_trans R x y <-> clos_trans_n1 R x y.
     Proof.
       split.
-      apply clos_trans_tn1.
-      apply clos_tn1_trans.
+      - apply clos_trans_tn1.
+      - apply clos_tn1_trans.
     Qed.
 
     (** Direct reflexive-transitive closure is equivalent to
@@ -203,31 +202,31 @@ Section Properties.
         clos_refl_trans_1n R x y -> clos_refl_trans R x y.
     Proof.
       induction 1.
-      constructor 2.
-      constructor 3 with y; auto.
-      constructor 1; auto.
+      - constructor 2.
+      - constructor 3 with y; auto.
+        constructor 1; auto.
     Qed.
 
     Lemma clos_rt_rt1n : forall x y,
         clos_refl_trans R x y -> clos_refl_trans_1n R x y.
     Proof.
       induction 1.
-      apply clos_rt1n_step; assumption.
-      left.
-      generalize IHclos_refl_trans2; clear IHclos_refl_trans2;
-        induction IHclos_refl_trans1; auto.
+      - apply clos_rt1n_step; assumption.
+      - left.
+      - generalize IHclos_refl_trans2; clear IHclos_refl_trans2;
+          induction IHclos_refl_trans1; auto.
 
-      right with y; auto.
-      eapply IHIHclos_refl_trans1; auto.
-      apply clos_rt1n_rt; auto.
+        right with y; auto.
+        eapply IHIHclos_refl_trans1; auto.
+        apply clos_rt1n_rt; auto.
     Qed.
 
     Lemma clos_rt_rt1n_iff : forall x y,
       clos_refl_trans R x y <-> clos_refl_trans_1n R x y.
     Proof.
       split.
-      apply clos_rt_rt1n.
-      apply clos_rt1n_rt.
+      - apply clos_rt_rt1n.
+      - apply clos_rt1n_rt.
     Qed.
 
     (** Direct reflexive-transitive closure is equivalent to
@@ -237,28 +236,28 @@ Section Properties.
         clos_refl_trans_n1 R x y -> clos_refl_trans R x y.
     Proof.
       induction 1.
-      constructor 2.
-      constructor 3 with y; auto.
-      constructor 1; assumption.
+      - constructor 2.
+      - constructor 3 with y; auto.
+        constructor 1; assumption.
     Qed.
 
     Lemma clos_rt_rtn1 :  forall x y,
         clos_refl_trans R x y -> clos_refl_trans_n1 R x y.
     Proof.
       induction 1.
-      apply clos_rtn1_step; auto.
-      left.
-      elim IHclos_refl_trans2; auto.
-      intros.
-      right with y0; auto.
+      - apply clos_rtn1_step; auto.
+      - left.
+      - elim IHclos_refl_trans2; auto.
+        intros.
+        right with y0; auto.
     Qed.
 
     Lemma clos_rt_rtn1_iff : forall x y,
         clos_refl_trans R x y <-> clos_refl_trans_n1 R x y.
     Proof.
       split.
-      apply clos_rt_rtn1.
-      apply clos_rtn1_rt.
+      - apply clos_rt_rtn1.
+      - apply clos_rtn1_rt.
     Qed.
 
     (** Induction on the left transitive step *)
@@ -271,14 +270,14 @@ Section Properties.
       intros.
       revert H H0.
       induction H1; intros; auto with sets.
-      apply H1 with x; auto with sets.
+      - apply H1 with x; auto with sets.
 
-      apply IHclos_refl_trans2.
-      apply IHclos_refl_trans1; auto with sets.
+      - apply IHclos_refl_trans2.
+        + apply IHclos_refl_trans1; auto with sets.
 
-      intros.
-      apply H0 with y0; auto with sets.
-      apply rt_trans with y; auto with sets.
+        + intros.
+          apply H0 with y0; auto with sets.
+          apply rt_trans with y; auto with sets.
     Qed.
 
     (** Induction on the right transitive step *)
@@ -311,45 +310,45 @@ Section Properties.
       clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y.
     Proof.
       induction 1.
-      constructor 2.
-      constructor 4 with y; auto.
-      case H;[constructor 1|constructor 3; constructor 1]; auto.
+      - constructor 2.
+      - constructor 4 with y; auto.
+        case H;[constructor 1|constructor 3; constructor 1]; auto.
     Qed.
 
     Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y ->
         clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n R x z.
       induction 1.
-      auto.
-      intros; right with y; eauto.
+      - auto.
+      - intros; right with y; eauto.
     Qed.
 
     Lemma clos_rst1n_sym : forall x y, clos_refl_sym_trans_1n R x y ->
       clos_refl_sym_trans_1n R y x.
     Proof.
       intros x y H; elim H.
-      constructor 1.
-      intros x0 y0 z D H0 H1; apply clos_rst1n_trans with y0; auto.
-      right with x0.
-      tauto.
-      left.
+      - constructor 1.
+      - intros x0 y0 z D H0 H1; apply clos_rst1n_trans with y0; auto.
+        right with x0.
+        + tauto.
+        + left.
     Qed.
 
     Lemma clos_rst_rst1n  : forall x y,
       clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y.
       induction 1.
-      constructor 2 with y; auto.
-      constructor 1.
-      constructor 1.
-      apply clos_rst1n_sym; auto.
-      eapply clos_rst1n_trans; eauto.
+      - constructor 2 with y; auto.
+        constructor 1.
+      - constructor 1.
+      - apply clos_rst1n_sym; auto.
+      - eapply clos_rst1n_trans; eauto.
     Qed.
 
     Lemma clos_rst_rst1n_iff : forall x y,
       clos_refl_sym_trans R x y <-> clos_refl_sym_trans_1n R x y.
     Proof.
       split.
-      apply clos_rst_rst1n.
-      apply clos_rst1n_rst.
+      - apply clos_rst_rst1n.
+      - apply clos_rst1n_rst.
     Qed.
 
     (** Direct reflexive-symmetric-transitive closure is equivalent to
@@ -359,9 +358,9 @@ Section Properties.
       clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans R x y.
     Proof.
       induction 1.
-      constructor 2.
-      constructor 4 with y; auto.
-      case H;[constructor 1|constructor 3; constructor 1]; auto.
+      - constructor 2.
+      - constructor 4 with y; auto.
+        case H;[constructor 1|constructor 3; constructor 1]; auto.
     Qed.
 
     Lemma clos_rstn1_trans : forall x y z, clos_refl_sym_trans_n1 R x y ->
@@ -369,39 +368,39 @@ Section Properties.
     Proof.
       intros x y z H1 H2.
       induction H2.
-      auto.
-      intros.
-      right with y0; eauto.
+      - auto.
+      - intros.
+        right with y0; eauto.
     Qed.
 
     Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y ->
       clos_refl_sym_trans_n1 R y x.
     Proof.
       intros x y H; elim H.
-      constructor 1.
-      intros y0 z D H0 H1. apply clos_rstn1_trans with y0; auto.
-      right with z.
-      tauto.
-      left.
+      - constructor 1.
+      - intros y0 z D H0 H1. apply clos_rstn1_trans with y0; auto.
+        right with z.
+        + tauto.
+        + left.
     Qed.
 
     Lemma clos_rst_rstn1 : forall x y,
       clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y.
     Proof.
       induction 1.
-      constructor 2 with x; auto.
-      constructor 1.
-      constructor 1.
-      apply clos_rstn1_sym; auto.
-      eapply clos_rstn1_trans; eauto.
+      - constructor 2 with x; auto.
+        constructor 1.
+      - constructor 1.
+      - apply clos_rstn1_sym; auto.
+      - eapply clos_rstn1_trans; eauto.
     Qed.
 
     Lemma clos_rst_rstn1_iff : forall x y,
       clos_refl_sym_trans R x y <-> clos_refl_sym_trans_n1 R x y.
     Proof.
       split.
-      apply clos_rst_rstn1.
-      apply clos_rstn1_rst.
+      - apply clos_rst_rstn1.
+      - apply clos_rstn1_rst.
     Qed.
 
   End Equivalences.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index f2475af124..862c3238e7 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -103,8 +103,8 @@ Section Ensembles_facts.
     forall (A:Ensemble U) (x y:U), In U (Add U A x) y -> In U A y \/ x = y.
   Proof.
     intros A x y H'; induction H'.
-      left; assumption.
-      right; apply Singleton_inv; assumption.
+    - left; assumption.
+    - right; apply Singleton_inv; assumption.
   Qed.
 
   Lemma Intersection_inv :
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 5b51c7b953..811e42f091 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -71,11 +71,11 @@ Section Partial_order_facts.
     elim D; simpl.
     intros C R H' H'0; elim H'0.
     intros H'1 H'2 H'3 x y z H'4 H'5; split.
-    apply H'2 with (y := y); tauto.
-    red; intro H'6.
-    elim H'4; intros H'7 H'8; apply H'8; clear H'4.
-    apply H'3; auto.
-    rewrite H'6; tauto.
+    - apply H'2 with (y := y); tauto.
+    - red; intro H'6.
+      elim H'4; intros H'7 H'8; apply H'8; clear H'4.
+      apply H'3; auto.
+      rewrite H'6; tauto.
   Qed.
 
   Lemma Strict_Rel_Transitive_with_Rel_left :
@@ -87,11 +87,11 @@ Section Partial_order_facts.
     elim D; simpl.
     intros C R H' H'0; elim H'0.
     intros H'1 H'2 H'3 x y z H'4 H'5; split.
-    apply H'2 with (y := y); tauto.
-    red; intro H'6.
-    elim H'5; intros H'7 H'8; apply H'8; clear H'5.
-    apply H'3; auto.
-    rewrite <- H'6; auto.
+    - apply H'2 with (y := y); tauto.
+    - red; intro H'6.
+      elim H'5; intros H'7 H'8; apply H'8; clear H'5.
+      apply H'3; auto.
+      rewrite <- H'6; auto.
   Qed.
 
   Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 86a500dfdd..5cd9f52c6b 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -33,8 +33,8 @@ Section Axiomatisation.
     forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).
   Proof.
     intros; apply cong_trans with (op y z).
-    apply cong_left; trivial.
-    apply cong_right; trivial.
+    - apply cong_left; trivial.
+    - apply cong_right; trivial.
   Qed.
 
   Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).
@@ -51,27 +51,27 @@ Section Axiomatisation.
   Proof.
     intros.
     apply cong_trans with (op x (op y z)).
-    apply op_ass.
-    apply cong_trans with (op x (op z y)).
-    apply cong_right; apply op_comm.
-    apply cong_sym; apply op_ass.
+    - apply op_ass.
+    - apply cong_trans with (op x (op z y)).
+      + apply cong_right; apply op_comm.
+      + apply cong_sym; apply op_ass.
   Qed.
 
   Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
   Proof.
     intros.
     apply cong_trans with (op (op x y) z).
-    apply cong_sym; apply op_ass.
-    apply cong_trans with (op (op y x) z).
-    apply cong_left; apply op_comm.
-    apply op_ass.
+    - apply cong_sym; apply op_ass.
+    - apply cong_trans with (op (op y x) z).
+      + apply cong_left; apply op_comm.
+      + apply op_ass.
   Qed.
 
   Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).
   Proof.
     intros; apply cong_trans with (op (op x y) z).
-    apply cong_sym; apply op_ass.
-    apply op_comm.
+    - apply cong_sym; apply op_ass.
+    - apply op_comm.
   Qed.
 
   (** Needed for treesort ... *)
@@ -80,10 +80,10 @@ Section Axiomatisation.
   Proof.
     intros.
     apply cong_trans with (op x (op (op y t) z)).
-    apply cong_right; apply perm_right.
-    apply cong_trans with (op (op x (op y t)) z).
-    apply cong_sym; apply op_ass.
-    apply cong_left; apply perm_left.
+    - apply cong_right; apply perm_right.
+    - apply cong_trans with (op (op x (op y t)) z).
+      + apply cong_sym; apply op_ass.
+      + apply cong_left; apply perm_left.
   Qed.
 
 End Axiomatisation.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 50a7e401f8..5b352f05fa 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -154,9 +154,9 @@ Theorem Union_is_Lub :
    Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
 intros A a b H' H'0.
 apply Lub_definition; simpl.
-apply Upper_Bound_definition; simpl; auto with sets.
-intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl; auto with sets.
+- apply Upper_Bound_definition; simpl; auto with sets.
+  intros y H'1; elim H'1; auto with sets.
+- intros y H'1; elim H'1; simpl; auto with sets.
 Qed.
 
 Theorem Intersection_is_Glb :
@@ -167,12 +167,12 @@ Theorem Intersection_is_Glb :
      (Intersection U a b).
 intros A a b H' H'0.
 apply Glb_definition; simpl.
-apply Lower_Bound_definition; simpl; auto with sets.
-apply Definition_of_Power_set.
-generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
- auto with sets.
-intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl; auto with sets.
+- apply Lower_Bound_definition; simpl; auto with sets.
+  + apply Definition_of_Power_set.
+    generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
+      auto with sets.
+  + intros y H'1; elim H'1; auto with sets.
+- intros y H'1; elim H'1; simpl; auto with sets.
 Qed.
 
 End The_power_set_partial_order.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 81b475ac6e..784f2ce0ff 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -84,8 +84,8 @@ Section Sets_as_an_algebra.
     forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
   Proof.
     intros x y; apply Extensionality_Ensembles; split; red.
-    intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
-    intros x0 H'; elim H'; auto with sets.
+    - intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
+    - intros x0 H'; elim H'; auto with sets.
   Qed.
 
   Theorem Triple_as_union :
@@ -94,10 +94,10 @@ Section Sets_as_an_algebra.
       Triple U x y z.
   Proof.
     intros x y z; apply Extensionality_Ensembles; split; red.
-    intros x0 H'; elim H'.
-    intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
-    intros x1 H'0; elim H'0; auto with sets.
-    intros x0 H'; elim H'; auto with sets.
+    - intros x0 H'; elim H'.
+      + intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
+      + intros x1 H'0; elim H'0; auto with sets.
+    - intros x0 H'; elim H'; auto with sets.
   Qed.
 
   Theorem Triple_as_Couple : forall x y:U, Couple U x y = Triple U x x y.
@@ -132,10 +132,10 @@ Section Sets_as_an_algebra.
     intros A B C.
     apply Extensionality_Ensembles.
     split; red; intros x H'.
-    elim H'.
-    intros x0 H'0 H'1; generalize H'0.
-    elim H'1; auto with sets.
-    elim H'; intros x0 H'0; elim H'0; auto with sets.
+    - elim H'.
+      intros x0 H'0 H'1; generalize H'0.
+      elim H'1; auto with sets.
+    - elim H'; intros x0 H'0; elim H'0; auto with sets.
   Qed.
 
   Lemma Distributivity_l
@@ -157,13 +157,13 @@ Section Sets_as_an_algebra.
     intros A B C.
     apply Extensionality_Ensembles.
     split; red; intros x H'.
-    elim H'; auto with sets.
-    intros x0 H'0; elim H'0; auto with sets.
-    elim H'.
-    intros x0 H'0; elim H'0; auto with sets.
-    intros x1 H'1 H'2; try exact H'2.
-    generalize H'1.
-    elim H'2; auto with sets.
+    - elim H'; auto with sets.
+      intros x0 H'0; elim H'0; auto with sets.
+    - elim H'.
+      intros x0 H'0; elim H'0; auto with sets.
+      intros x1 H'1 H'2; try exact H'2.
+      generalize H'1.
+      elim H'2; auto with sets.
   Qed.
 
   Theorem Union_add :
@@ -188,11 +188,11 @@ Section Sets_as_an_algebra.
     intros X x H'; unfold Subtract.
     apply Extensionality_Ensembles.
     split; red; auto with sets.
-    intros x0 H'0; elim H'0; auto with sets.
-    intros x0 H'0; apply Setminus_intro; auto with sets.
-    red; intro H'1; elim H'1.
-    lapply (Singleton_inv U x x0); auto with sets.
-    intro H'4; apply H'; rewrite H'4; auto with sets.
+    - intros x0 H'0; elim H'0; auto with sets.
+    - intros x0 H'0; apply Setminus_intro; auto with sets.
+      red; intro H'1; elim H'1.
+      lapply (Singleton_inv U x x0); auto with sets.
+      intro H'4; apply H'; rewrite H'4; auto with sets.
   Qed.
 
   Lemma singlx : forall x y:U, In U (Add U (Empty_set U) x) y -> x = y.
@@ -320,7 +320,9 @@ Section Sets_as_an_algebra.
     Setminus A s1 (Union A s2 s3) = Setminus A (Setminus A s1 s2) s3.
   Proof.
     intros. apply Extensionality_Ensembles. split.
-    * intros x H. inversion H. constructor. intuition. contradict H1. intuition.
+    * intros x H. inversion H. constructor.
+      -- intuition.
+      -- contradict H1. intuition.
     * intros x H. inversion H. inversion H0. constructor; intuition. inversion H4; intuition.
   Qed.
 
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index d275487e15..17bdefcdbf 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -45,12 +45,12 @@ Theorem Equiv_from_preorder :
 Proof.
 intros U R H'; elim H'; intros H'0 H'1.
 apply Definition_of_equivalence.
-red in H'0; auto 10 with sets.
-2: red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
-red in H'1; red; auto 10 with sets.
-intros x y z h; elim h; intros H'3 H'4; clear h.
-intro h; elim h; intros H'5 H'6; clear h.
-split; apply H'1 with y; auto 10 with sets.
+- red in H'0; auto 10 with sets.
+- red in H'1; red; auto 10 with sets.
+  intros x y z h; elim h; intros H'3 H'4; clear h.
+  intro h; elim h; intros H'5 H'6; clear h.
+  split; apply H'1 with y; auto 10 with sets.
+- red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
 Qed.
 Hint Resolve Equiv_from_preorder : core.
 
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 36da368447..48d0ea55c9 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -53,8 +53,8 @@ Theorem Rstar_contains_Rplus :
 Proof.
 intros U R; red.
 intros x y H'; elim H'.
-generalize Rstar_contains_R; intro T; red in T; auto with sets.
-intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets.
+- generalize Rstar_contains_R; intro T; red in T; auto with sets.
+- intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets.
 Qed.
 
 Theorem Rstar_transitive :
@@ -79,9 +79,9 @@ Proof.
 generalize Rstar_contains_R; intro T; red in T.
 intros U R; unfold same_relation, contains.
 split; intros x y H'; elim H'; auto with sets.
-generalize Rstar_transitive; intro T1; red in T1.
-intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets.
-intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets.
+- generalize Rstar_transitive; intro T1; red in T1.
+  intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets.
+- intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets.
 Qed.
 
 Theorem Rsym_imp_Rstarsym :
@@ -121,12 +121,12 @@ Proof.
 generalize Rstar_contains_Rplus; intro T; red in T.
 generalize Rstar_transitive; intro T1; red in T1.
 intros U R x y z H'; elim H'.
-intros x0 H'0; elim H'0.
-intros x1 y0 H'1; exists y0; auto with sets.
-intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets.
-intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0.
-split; [ try assumption | idtac ].
-apply T1 with z0; auto with sets.
+- intros x0 H'0; elim H'0.
+  + intros x1 y0 H'1; exists y0; auto with sets.
+  + intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets.
+- intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0.
+  split; [ try assumption | idtac ].
+  apply T1 with z0; auto with sets.
 Qed.
 
 Theorem Lemma1 :
@@ -137,17 +137,17 @@ Theorem Lemma1 :
      forall a:U, R x a ->  exists z : _, Rstar U R a z /\ R b z.
 Proof.
 intros U R H' x b H'0; elim H'0.
-intros x0 a H'1; exists a; auto with sets.
-intros x0 y z H'1 H'2 H'3 a H'4.
-red in H'.
-specialize H' with (x := x0) (a := a) (b := y); lapply H';
- [ intro H'8; lapply H'8;
-    [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
- | clear H' ]; auto with sets.
-elim H'9.
-intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
-elim (H'3 t); auto with sets.
-intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
-exists z1; split; [ idtac | assumption ].
-apply Rstar_n with t; auto with sets.
+- intros x0 a H'1; exists a; auto with sets.
+- intros x0 y z H'1 H'2 H'3 a H'4.
+  red in H'.
+  specialize H' with (x := x0) (a := a) (b := y); lapply H';
+    [ intro H'8; lapply H'8;
+      [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
+    | clear H' ]; auto with sets.
+  elim H'9.
+  intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
+  elim (H'3 t); auto with sets.
+  intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
+  exists z1; split; [ idtac | assumption ].
+  apply Rstar_n with t; auto with sets.
 Qed.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 18ea019526..a4806ea0a6 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -57,21 +57,21 @@ intro x; red; intros a b H'0.
 unfold coherent at 1.
 generalize b; clear b.
 elim H'0; clear H'0.
-intros x0 b H'1; exists b; auto with sets.
-intros x0 y z H'1 H'2 H'3 b H'4.
-generalize (Lemma1 U R); intro h; lapply h;
- [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0;
-    [ intro H'5; generalize (H'5 y); intro h1; lapply h1;
-       [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7;
+- intros x0 b H'1; exists b; auto with sets.
+- intros x0 y z H'1 H'2 H'3 b H'4.
+  generalize (Lemma1 U R); intro h; lapply h;
+    [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0;
+      [ intro H'5; generalize (H'5 y); intro h1; lapply h1;
+        [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7;
           clear h h0 h1 h2 h3
-       | clear h h0 h1 ]
-    | clear h h0 ]
- | clear h ]; auto with sets.
-generalize (H'3 z0); intro h; lapply h;
- [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1
- | clear h ]; auto with sets.
-exists z1; split; auto with sets.
-apply Rstar_n with z0; auto with sets.
+        | clear h h0 h1 ]
+      | clear h h0 ]
+    | clear h ]; auto with sets.
+  generalize (H'3 z0); intro h; lapply h;
+    [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1
+    | clear h ]; auto with sets.
+  exists z1; split; auto with sets.
+  apply Rstar_n with z0; auto with sets.
 Qed.
 
 Theorem Strong_confluence_direct :
@@ -82,31 +82,31 @@ intro x; red; intros a b H'0.
 unfold coherent at 1.
 generalize b; clear b.
 elim H'0; clear H'0.
-intros x0 b H'1; exists b; auto with sets.
-intros x0 y z H'1 H'2 H'3 b H'4.
-cut (ex (fun t:U => Rstar U R y t /\ R b t)).
-intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0.
-generalize (H'3 t); intro h; lapply h;
- [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1
- | clear h ]; auto with sets.
-exists z0; split; [ assumption | idtac ].
-apply Rstar_n with t; auto with sets.
-generalize H'1; generalize y; clear H'1.
-elim H'4.
-intros x1 y0 H'0; exists y0; auto with sets.
-intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
-red in H'.
-generalize (H' x1 y0 y1); intro h; lapply h;
- [ intro H'7; lapply H'7;
-    [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9;
-       clear h H'7 h0 h1
-    | clear h ]
- | clear h ]; auto with sets.
-generalize (H'5 z1); intro h; lapply h;
- [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1
- | clear h ]; auto with sets.
-exists t; split; auto with sets.
-apply Rstar_n with z1; auto with sets.
+- intros x0 b H'1; exists b; auto with sets.
+- intros x0 y z H'1 H'2 H'3 b H'4.
+  cut (ex (fun t:U => Rstar U R y t /\ R b t)).
+  + intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0.
+    generalize (H'3 t); intro h; lapply h;
+      [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1
+      | clear h ]; auto with sets.
+    exists z0; split; [ assumption | idtac ].
+    apply Rstar_n with t; auto with sets.
+  + generalize H'1; generalize y; clear H'1.
+    elim H'4.
+    * intros x1 y0 H'0; exists y0; auto with sets.
+    * intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.
+      red in H'.
+      generalize (H' x1 y0 y1); intro h; lapply h;
+        [ intro H'7; lapply H'7;
+          [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9;
+            clear h H'7 h0 h1
+          | clear h ]
+        | clear h ]; auto with sets.
+      generalize (H'5 z1); intro h; lapply h;
+        [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1
+        | clear h ]; auto with sets.
+      exists t; split; auto with sets.
+      apply Rstar_n with z1; auto with sets.
 Qed.
 
 Theorem Noetherian_contains_Noetherian :
@@ -131,41 +131,41 @@ generalize (Rstar_cases U R x0 y); intro h; lapply h;
     | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6;
        clear h h0 h1 h2 ]
  | clear h ]; auto with sets.
-elim h1; auto with sets.
-generalize (Rstar_cases U R x0 z); intro h; lapply h;
- [ intro h0; elim h0;
-    [ clear h h0; intro h1
-    | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8;
-       clear h h0 h1 h2 ]
- | clear h ]; auto with sets.
-elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets.
-unfold Locally_confluent, locally_confluent, coherent in H'0.
-generalize (H'0 x0 u v); intro h; lapply h;
- [ intro H'9; lapply H'9;
-    [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11;
-       clear h H'9 h0 h1
-    | clear h ]
- | clear h ]; auto with sets.
-clear H'0.
-unfold coherent at 1 in H'2.
-generalize (H'2 u); intro h; lapply h;
- [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
-    [ intro H'9; lapply H'9;
-       [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13;
-          clear h h0 H'9 h1 h2
-       | clear h h0 ]
-    | clear h h0 ]
- | clear h ]; auto with sets.
-generalize Rstar_transitive; intro T; red in T.
-generalize (H'2 v); intro h; lapply h;
- [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0;
-    [ intro H'14; lapply H'14;
-       [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16;
-          clear h h0 H'14 h1 h2
-       | clear h h0 ]
-    | clear h h0 ]
- | clear h ]; auto with sets.
-red; (exists z1; split); auto with sets.
-apply T with y1; auto with sets.
-apply T with t; auto with sets.
+- elim h1; auto with sets.
+- generalize (Rstar_cases U R x0 z); intro h; lapply h;
+    [ intro h0; elim h0;
+      [ clear h h0; intro h1
+      | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8;
+        clear h h0 h1 h2 ]
+    | clear h ]; auto with sets.
+  + elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets.
+  + unfold Locally_confluent, locally_confluent, coherent in H'0.
+    generalize (H'0 x0 u v); intro h; lapply h;
+      [ intro H'9; lapply H'9;
+        [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11;
+          clear h H'9 h0 h1
+        | clear h ]
+      | clear h ]; auto with sets.
+    clear H'0.
+    unfold coherent at 1 in H'2.
+    generalize (H'2 u); intro h; lapply h;
+      [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
+        [ intro H'9; lapply H'9;
+          [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13;
+            clear h h0 H'9 h1 h2
+          | clear h h0 ]
+        | clear h h0 ]
+      | clear h ]; auto with sets.
+    generalize Rstar_transitive; intro T; red in T.
+    generalize (H'2 v); intro h; lapply h;
+      [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0;
+        [ intro H'14; lapply H'14;
+          [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16;
+            clear h h0 H'14 h1 h2
+          | clear h h0 ]
+        | clear h h0 ]
+      | clear h ]; auto with sets.
+    * red; (exists z1; split); auto with sets.
+      apply T with y1; auto with sets.
+    * apply T with t; auto with sets.
 Qed.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 0ff304ed6b..edfffe6ce9 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -174,8 +174,8 @@ Lemma uniset_twist2 :
    seq (union x (union (union y z) t)) (union (union y (union x z)) t).
 Proof.
 intros; apply seq_trans with (union (union x (union y z)) t).
-apply seq_sym; apply union_ass.
-apply seq_left; apply union_perm_left.
+- apply seq_sym; apply union_ass.
+- apply seq_left; apply union_perm_left.
 Qed.
 
 (** specific for treesort *)
@@ -186,8 +186,8 @@ Lemma treesort_twist1 :
    seq (union x (union u t)) (union (union y (union x t)) z).
 Proof.
 intros; apply seq_trans with (union x (union (union y z) t)).
-apply seq_right; apply seq_left; trivial.
-apply uniset_twist1.
+- apply seq_right; apply seq_left; trivial.
+- apply uniset_twist1.
 Qed.
 
 Lemma treesort_twist2 :
@@ -196,8 +196,8 @@ Lemma treesort_twist2 :
    seq (union x (union u t)) (union (union y (union x z)) t).
 Proof.
 intros; apply seq_trans with (union x (union (union y z) t)).
-apply seq_right; apply seq_left; trivial.
-apply uniset_twist2.
+- apply seq_right; apply seq_left; trivial.
+- apply uniset_twist2.
 Qed.
 
 
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 4143dba547..346c300ee5 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -158,8 +158,10 @@ Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
  Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
  Proof.
   intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ].
-  auto with *.
-  split. discriminate. intro EQ; elim NEQ; auto.
+  - auto with *.
+  - split.
+    + discriminate.
+    + intro EQ; elim NEQ; auto.
  Qed.
 End HasEqDec2Bool.
 
@@ -168,8 +170,8 @@ Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
  Proof.
   intros x y. assert (H:=F.eqb_eq x y).
   destruct (F.eqb x y); [left|right].
-  apply -> H; auto.
-  intro EQ. apply H in EQ. discriminate.
+  - apply -> H; auto.
+  - intro EQ. apply H in EQ. discriminate.
  Defined.
 End HasEqBool2Dec.
 
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 4d04667c01..c314f3f982 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -47,8 +47,8 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O.
  intros H H'.
  apply (StrictOrder_Irreflexive x).
  rewrite le_lteq in *; destruct H as [H|H].
- transitivity y; auto.
- rewrite H in H'; auto.
+ - transitivity y; auto.
+ - rewrite H in H'; auto.
  Qed.
 
  Lemma max_l x y : y<=x -> max x y == x.
@@ -142,8 +142,8 @@ Proof.
  intros Eqf Lef x y.
  destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
- assert (f x <= f y) by (apply Lef; order). order.
- assert (f y <= f x) by (apply Lef; order). order.
+ - assert (f x <= f y) by (apply Lef; order). order.
+ - assert (f y <= f x) by (apply Lef; order). order.
 Qed.
 
 (** *** Semi-lattice algebraic properties of [max] *)
@@ -194,7 +194,11 @@ Proof.
 Qed.
 
 Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m.
-Proof. split. apply max_le. solve_max. Qed.
+Proof.
+  split.
+  - apply max_le.
+  - solve_max.
+Qed.
 
 Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m.
 Proof.
@@ -282,8 +286,8 @@ Proof.
  intros Eqf Lef x y.
  destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
- assert (f x <= f y) by (apply Lef; order). order.
- assert (f y <= f x) by (apply Lef; order). order.
+ - assert (f x <= f y) by (apply Lef; order). order.
+ - assert (f y <= f x) by (apply Lef; order). order.
 Qed.
 
 Lemma min_id n : min n n == n.
@@ -330,7 +334,11 @@ Proof.
 Qed.
 
 Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p.
-Proof. split. apply min_le. solve_min. Qed.
+Proof.
+  split.
+  - apply min_le.
+  - solve_min.
+Qed.
 
 Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p.
 Proof.
@@ -377,16 +385,16 @@ Lemma min_max_absorption n m : max n (min n m) == n.
 Proof.
  intros.
  destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E.
- apply max_l. order.
- destruct (max_spec n m); intuition; order.
+ - apply max_l. order.
+ - destruct (max_spec n m); intuition; order.
 Qed.
 
 Lemma max_min_absorption n m : min n (max n m) == n.
 Proof.
  intros.
  destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E.
- destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order.
- apply min_l; auto. order.
+ - destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order.
+ - apply min_l; auto. order.
 Qed.
 
 (** Distributivity *)
@@ -395,16 +403,16 @@ Lemma max_min_distr n m p :
  max n (min m p) == min (max n m) (max n p).
 Proof.
  symmetry. apply min_mono.
- eauto with *.
- repeat red; intros. apply max_le_compat_l; auto.
+ - eauto with *.
+ - repeat red; intros. apply max_le_compat_l; auto.
 Qed.
 
 Lemma min_max_distr n m p :
  min n (max m p) == max (min n m) (min n p).
 Proof.
  symmetry. apply max_mono.
- eauto with *.
- repeat red; intros. apply min_le_compat_l; auto.
+ - eauto with *.
+ - repeat red; intros. apply min_le_compat_l; auto.
 Qed.
 
 (** Modularity *)
@@ -415,8 +423,8 @@ Proof.
  rewrite <- max_min_distr.
  destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.
  destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.
- rewrite 2 max_l; try order. rewrite min_le_iff; auto.
- rewrite 2 max_l; try order. rewrite min_le_iff; auto.
+ - rewrite 2 max_l; try order. rewrite min_le_iff; auto.
+ - rewrite 2 max_l; try order. rewrite min_le_iff; auto.
 Qed.
 
 Lemma min_max_modular n m p :
@@ -425,8 +433,8 @@ Proof.
  intros. rewrite <- min_max_distr.
  destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.
  destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'.
- rewrite 2 min_l; try order. rewrite max_le_iff; right; order.
- rewrite 2 min_l; try order. rewrite max_le_iff; auto.
+ - rewrite 2 min_l; try order. rewrite max_le_iff; right; order.
+ - rewrite 2 min_l; try order. rewrite max_le_iff; auto.
 Qed.
 
 (** Disassociativity *)
@@ -448,8 +456,8 @@ Proof.
  intros Eqf Lef x y.
  destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
- assert (f y <= f x) by (apply Lef; order). order.
- assert (f x <= f y) by (apply Lef; order). order.
+ - assert (f y <= f x) by (apply Lef; order). order.
+ - assert (f x <= f y) by (apply Lef; order). order.
 Qed.
 
 Lemma min_max_antimono f :
@@ -460,8 +468,8 @@ Proof.
  intros Eqf Lef x y.
  destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
- assert (f y <= f x) by (apply Lef; order). order.
- assert (f x <= f y) by (apply Lef; order). order.
+ - assert (f y <= f x) by (apply Lef; order). order.
+ - assert (f x <= f y) by (apply Lef; order). order.
 Qed.
 
 End MinMaxLogicalProperties.
@@ -479,12 +487,12 @@ Lemma max_case_strong n m (P:t -> Type) :
 Proof.
 intros Compat Hl Hr.
 destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
-assert (n<=m) by (rewrite le_lteq; auto).
-apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
-assert (n<=m) by (rewrite le_lteq; auto).
-apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
-assert (m<=n) by (rewrite le_lteq; auto).
-apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
+- assert (n<=m) by (rewrite le_lteq; auto).
+  apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
+- assert (n<=m) by (rewrite le_lteq; auto).
+  apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
+- assert (m<=n) by (rewrite le_lteq; auto).
+  apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
 Defined.
 
 Lemma max_case n m (P:t -> Type) :
@@ -508,12 +516,12 @@ Lemma min_case_strong n m (P:O.t -> Type) :
 Proof.
 intros Compat Hl Hr.
 destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
-assert (n<=m) by (rewrite le_lteq; auto).
-apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
-assert (n<=m) by (rewrite le_lteq; auto).
-apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
-assert (m<=n) by (rewrite le_lteq; auto).
-apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
+- assert (n<=m) by (rewrite le_lteq; auto).
+  apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
+- assert (n<=m) by (rewrite le_lteq; auto).
+  apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
+- assert (m<=n) by (rewrite le_lteq; auto).
+  apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
 Defined.
 
 Lemma min_case n m (P:O.t -> Type) :
@@ -624,11 +632,11 @@ Module TOMaxEqDec_to_Compare
  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
  intros; unfold compare; repeat destruct eq_dec; auto; constructor.
- destruct (lt_total x y); auto.
- absurd (x==y); auto. transitivity (max x y); auto.
- symmetry. apply max_l. rewrite le_lteq; intuition.
- destruct (lt_total y x); auto.
- absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition.
+ - destruct (lt_total x y); auto.
+   absurd (x==y); auto. transitivity (max x y); auto.
+   symmetry. apply max_l. rewrite le_lteq; intuition.
+ - destruct (lt_total y x); auto.
+   absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition.
  Qed.
 
 End TOMaxEqDec_to_Compare.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 310a22a0a4..7fcf517457 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -143,8 +143,8 @@ Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.
  Proof.
  unfold eqb. intros x y.
  destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate.
- intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
- intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ - intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
  Qed.
 
 End Compare2EqBool.
@@ -252,9 +252,11 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
  Proof.
  intros. unfold leb. rewrite le_lteq.
  destruct (compare_spec x y) as [EQ|LT|GT]; split; auto.
- discriminate.
- intros LE. elim (StrictOrder_Irreflexive x).
- destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT.
+ - discriminate.
+ - intros LE. elim (StrictOrder_Irreflexive x).
+   destruct LE as [LT|EQ].
+   + now transitivity y.
+   + now rewrite <- EQ in GT.
  Qed.
 
  Lemma leb_total : forall x y, leb x y \/ leb y x.
@@ -267,10 +269,10 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
  Proof.
  intros x y z. rewrite !leb_le, !le_lteq.
  intros [Hxy|Hxy] [Hyz|Hyz].
- left; transitivity y; auto.
- left; rewrite <- Hyz; auto.
- left; rewrite Hxy; auto.
- right; transitivity y; auto.
+ - left; transitivity y; auto.
+ - left; rewrite <- Hyz; auto.
+ - left; rewrite Hxy; auto.
+ - right; transitivity y; auto.
  Qed.
 
  Definition t := t.
@@ -302,10 +304,10 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
  Proof.
  intros. unfold compare.
  case_eq (x <=? y).
- case_eq (y <=? x).
- constructor. split; auto.
- constructor. split; congruence.
- constructor. destruct (leb_total x y); split; congruence.
+ - case_eq (y <=? x).
+   + constructor. split; auto.
+   + constructor. split; congruence.
+ - constructor. destruct (leb_total x y); split; congruence.
  Qed.
 
  Definition eqb x y := (x <=? y) && (y <=? x).
@@ -321,19 +323,19 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
  Instance eq_equiv : Equivalence eq.
  Proof.
  split.
- intros x; unfold eq, le. destruct (leb_total x x); auto.
- intros x y; unfold eq, le. intuition.
- intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto.
+ - intros x; unfold eq, le. destruct (leb_total x x); auto.
+ - intros x y; unfold eq, le. intuition.
+ - intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto.
  Qed.
 
  Instance lt_strorder : StrictOrder lt.
  Proof.
  split.
- intros x. unfold lt; red; intuition.
- intros x y z; unfold lt, le. intuition.
- apply leb_trans with y; auto.
- absurd (z <=? y); auto.
- apply leb_trans with x; auto.
+ - intros x. unfold lt; red; intuition.
+ - intros x y z; unfold lt, le. intuition.
+   + apply leb_trans with y; auto.
+   + absurd (z <=? y); auto.
+     apply leb_trans with x; auto.
  Qed.
 
  Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
@@ -341,11 +343,11 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
  apply proper_sym_impl_iff_2; auto with *.
  intros x x' Hx y y' Hy' H. unfold eq, lt, le in *.
  intuition.
- apply leb_trans with x; auto.
- apply leb_trans with y; auto.
- absurd (y <=? x); auto.
- apply leb_trans with x'; auto.
- apply leb_trans with y'; auto.
+ - apply leb_trans with x; auto.
+   apply leb_trans with y; auto.
+ - absurd (y <=? x); auto.
+   apply leb_trans with x'; auto.
+   apply leb_trans with y'; auto.
  Qed.
 
  Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 1fb0a37e16..182b781fe1 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -290,9 +290,9 @@ Module Type CompareBasedOrderFacts
  Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y).
  Proof.
   case_eq (compare x y); intros H; constructor.
-  now apply compare_eq_iff.
-  now apply compare_lt_iff.
-  rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff.
+  - now apply compare_eq_iff.
+  - now apply compare_lt_iff.
+  - rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff.
  Qed.
 
  Lemma compare_eq x y : (x ?= y) = Eq -> x==y.
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 10d9027435..ea7769a994 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -45,11 +45,11 @@ Section Wf_Disjoint_Union.
     intros.
     unfold well_founded.
     destruct a as [a| b].
-    apply (acc_A_sum a).
-    apply (H a).
+    - apply (acc_A_sum a).
+      apply (H a).
 
-    apply (acc_B_sum H b).
-    apply (H0 b).
+    - apply (acc_B_sum H b).
+      apply (H0 b).
   Qed.
 
 End Wf_Disjoint_Union.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 37fd2fb23f..b2d08186ea 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -36,23 +36,23 @@ Section WfLexicographic_Product.
     apply Acc_intro.
     destruct y as [x2 y1]; intro H6.
     simple inversion H6; intro.
-    cut (leA x2 x); intros.
-    apply IHAcc; auto with sets.
-    intros.
-    apply H2.
-    apply t_trans with x2; auto with sets.
-
-    red in H2.
-    apply H2.
-    auto with sets.
-
-    injection H1 as <- _.
-    injection H3 as <- _; auto with sets.
-
-    rewrite <- H1.
-    injection H3 as -> H3.
-    apply IHAcc0.
-    elim inj_pair2 with A B x y' x0; assumption.
+    - cut (leA x2 x); intros.
+      + apply IHAcc; auto with sets.
+        * intros.
+          apply H2.
+          apply t_trans with x2; auto with sets.
+
+        * red in H2.
+          apply H2.
+          auto with sets.
+
+      + injection H1 as <- _.
+        injection H3 as <- _; auto with sets.
+
+    - rewrite <- H1.
+      injection H3 as -> H3.
+      apply IHAcc0.
+      elim inj_pair2 with A B x y' x0; assumption.
   Defined.
 
   Theorem wf_lexprod :
@@ -116,17 +116,17 @@ Section Swap.
     apply Acc_intro.
     destruct y0; intros.
     inversion_clear H; inversion_clear H1; apply H0.
-    apply sp_swap.
-    apply right_sym; auto with sets.
+    - apply sp_swap.
+      apply right_sym; auto with sets.
 
-    apply sp_swap.
-    apply left_sym; auto with sets.
+    - apply sp_swap.
+      apply left_sym; auto with sets.
 
-    apply sp_noswap.
-    apply right_sym; auto with sets.
+    - apply sp_noswap.
+      apply right_sym; auto with sets.
 
-    apply sp_noswap.
-    apply left_sym; auto with sets.
+    - apply sp_noswap.
+      apply left_sym; auto with sets.
   Defined.
 
 
@@ -135,26 +135,26 @@ Section Swap.
   Proof.
     induction 1 as [x0 _ IHAcc0]; intros H2.
     cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)).
-    clear IHAcc0.
-    induction H2 as [x1 _ IHAcc1]; intros H4.
-    cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
-    clear IHAcc1.
-    intro.
-    apply Acc_intro.
-    destruct y; intro H5.
-    inversion_clear H5.
-    inversion_clear H0; auto with sets.
-
-    apply swap_Acc.
-    inversion_clear H0; auto with sets.
-
-    intros.
-    apply IHAcc1; auto with sets; intros.
-    apply Acc_inv with (y0, x1); auto with sets.
-    apply sp_noswap.
-    apply right_sym; auto with sets.
-
-    auto with sets.
+    - clear IHAcc0.
+      induction H2 as [x1 _ IHAcc1]; intros H4.
+      cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
+      + clear IHAcc1.
+        intro.
+        apply Acc_intro.
+        destruct y; intro H5.
+        inversion_clear H5.
+        * inversion_clear H0; auto with sets.
+
+        * apply swap_Acc.
+          inversion_clear H0; auto with sets.
+
+      + intros.
+        apply IHAcc1; auto with sets; intros.
+        apply Acc_inv with (y0, x1); auto with sets.
+        apply sp_noswap.
+        apply right_sym; auto with sets.
+
+    - auto with sets.
   Defined.
 
 
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 9e671651fa..14d425b811 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -27,13 +27,13 @@ Section WfUnion.
       forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & clos_trans A R1 z y'.
   Proof.
     induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
-    elim H with y x z; auto with sets; intros x0 H2 H3.
-    exists x0; auto with sets.
+    - elim H with y x z; auto with sets; intros x0 H2 H3.
+      exists x0; auto with sets.
 
-    elim IH1 with z0; auto with sets; intros.
-    elim IH2 with x0; auto with sets; intros.
-    exists x1; auto with sets.
-    apply t_trans with x0; auto with sets.
+    - elim IH1 with z0; auto with sets; intros.
+      elim IH2 with x0; auto with sets; intros.
+      exists x1; auto with sets.
+      apply t_trans with x0; auto with sets.
   Qed.
 
 
@@ -46,21 +46,21 @@ Section WfUnion.
     elim H3; intros; auto with sets.
     cut (clos_trans A R1 y x); auto with sets.
     elimtype (Acc (clos_trans A R1) y); intros.
-    apply Acc_intro; intros.
-    elim H8; intros.
-    apply H6; auto with sets.
-    apply t_trans with x0; auto with sets.
+    - apply Acc_intro; intros.
+      elim H8; intros.
+      + apply H6; auto with sets.
+        apply t_trans with x0; auto with sets.
 
-    elim strip_commut with x x0 y0; auto with sets; intros.
-    apply Acc_inv_trans with x1; auto with sets.
-    unfold union.
-    elim H11; auto with sets; intros.
-    apply t_trans with y1; auto with sets.
+      + elim strip_commut with x x0 y0; auto with sets; intros.
+        apply Acc_inv_trans with x1; auto with sets.
+        unfold union.
+        elim H11; auto with sets; intros.
+        apply t_trans with y1; auto with sets.
 
-    apply (Acc_clos_trans A).
-    apply Acc_inv with x; auto with sets.
-    apply H0.
-    apply Acc_intro; auto with sets.
+    - apply (Acc_clos_trans A).
+      apply Acc_inv with x; auto with sets.
+      apply H0.
+      apply Acc_intro; auto with sets.
   Qed.
 
 
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index cf46657d36..eb98fb2aba 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -39,9 +39,9 @@ Section WellOrdering.
     intros.
     apply (H v0 y0).
     cut (f = f1).
-    intros E; rewrite E; auto.
-    symmetry .
-    apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
+    - intros E; rewrite E; auto.
+    - symmetry .
+      apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
   Qed.
 
 End WellOrdering.