Small Linting of the code base to have a tab of 2

theories/Arith/Arith_base.v

@@ -287,7 +287,7 @@ Hint Resolve minus_diag_reverse_stt: arith. (* Minus.minus_diag_reverse *)
 #[local]
 Lemma minus_plus_simpl_l_reverse_stt n m p : n - m = p + n - (p + m).
 Proof.
- now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub.
+  now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub.
 Qed.
 Add Search Blacklist "Coq.Arith.Arith_base.minus_plus_simpl_l_reverse_stt".
 #[global]
@@ -346,7 +346,7 @@ Hint Resolve mult_assoc_reverse_stt Nat.mul_assoc: arith. (* Mult.mult_assoc_rev
 #[local]
 Lemma mult_O_le_stt n m : m = 0 \/ n <= m * n.
 Proof.
- destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
+  destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
 Qed.
 Add Search Blacklist "Coq.Arith.Arith_base.mult_O_le_stt".
 #[global]

theories/Arith/Compare_dec.v

@@ -160,22 +160,22 @@ Notation nat_compare_S := Nat.compare_succ (only parsing).
 
 Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.
 Proof.
- symmetry. apply Nat.compare_lt_iff.
+  symmetry. apply Nat.compare_lt_iff.
 Qed.
 
 Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt.
 Proof.
- symmetry. apply Nat.compare_gt_iff.
+  symmetry. apply Nat.compare_gt_iff.
 Qed.
 
 Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt.
 Proof.
- symmetry. apply Nat.compare_le_iff.
+  symmetry. apply Nat.compare_le_iff.
 Qed.
 
 Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt.
 Proof.
- symmetry. apply Nat.compare_ge_iff.
+  symmetry. apply Nat.compare_ge_iff.
 Qed.
 
 (** Some projections of the above equivalences. *)
@@ -223,30 +223,30 @@ Notation leb_iff := Nat.leb_le (only parsing).
 
 Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n.
 Proof.
- rewrite Nat.leb_nle. apply Nat.nle_gt.
+  rewrite Nat.leb_nle. apply Nat.nle_gt.
 Qed.
 
 Lemma leb_correct m n : m <= n -> (m <=? n) = true.
 Proof.
- apply Nat.leb_le.
+  apply Nat.leb_le.
 Qed.
 
 Lemma leb_complete m n : (m <=? n) = true -> m <= n.
 Proof.
- apply Nat.leb_le.
+  apply Nat.leb_le.
 Qed.
 
 Lemma leb_correct_conv m n : m < n -> (n <=? m) = false.
 Proof.
- apply leb_iff_conv.
+  apply leb_iff_conv.
 Qed.
 
 Lemma leb_complete_conv m n : (n <=? m) = false -> m < n.
 Proof.
- apply leb_iff_conv.
+  apply leb_iff_conv.
 Qed.
 
 Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt.
 Proof.
- rewrite Nat.compare_le_iff. apply Nat.leb_le.
+  rewrite Nat.compare_le_iff. apply Nat.leb_le.
 Qed.

theories/Arith/EqNat.v

@@ -39,12 +39,12 @@ Qed.
 
 Lemma eq_eq_nat n m : n = m -> eq_nat n m.
 Proof.
- apply eq_nat_is_eq.
+  apply eq_nat_is_eq.
 Qed.
 
 Lemma eq_nat_eq n m : eq_nat n m -> n = m.
 Proof.
- apply eq_nat_is_eq.
+  apply eq_nat_is_eq.
 Qed.
 
 Theorem eq_nat_elim :

theories/Arith/Factorial.v

@@ -29,7 +29,7 @@ Qed.
 
 Lemma fact_neq_0 n : fact n <> 0.
 Proof.
- apply Nat.neq_0_lt_0, lt_O_fact.
+  apply Nat.neq_0_lt_0, lt_O_fact.
 Qed.
 
 Lemma fact_le n m : n <= m -> fact n <= fact m.