[doc] [cleanup] Made sqrt2 main proof a bit more verbose.

It is longer, yes, but perhaps easier to understand in prose.
Fixed indentation.

examples/sqrt2.v

@@ -13,7 +13,7 @@ version of a #<a href="https://github.com/coq-community/qarith-stern-brocot/blob
 We begin by loading results on arithmetic on natural numbers,
 and the lia arithmetic solver tactic.
 *)
-From Coq Require Import Arith Lia.
+From Coq Require Import Utf8 Arith Lia.
 
 (** ** Arithmetic utility results *)
 
@@ -23,16 +23,17 @@ Lemma lt_monotonic_inverse :
   forall x y : nat, f x < f y -> x < y.
 Proof.
   intros f Hmon x y Hlt; case (le_gt_dec y x); auto.
-intros Hle; case (proj1 (Nat.lt_eq_cases _ _) Hle).
-intros Hlt'; case (Nat.lt_asymm _ _ Hlt); apply Hmon; auto.
-intros Heq; case (Nat.lt_neq _ _ Hlt); rewrite Heq; auto.
+  intros Hle; elim (le_lt_or_eq _ _ Hle).
+  intros Hlt'; elim (lt_asym _ _ Hlt); apply Hmon; auto.
+  intros Heq; elim (Nat.lt_neq _ _ Hlt); rewrite Heq; auto.
 Qed.
 
+(** The lia tactic easily proves linear arithmetic statements. *)
 Lemma sub_square_identity :
  forall a b : nat, b <= a -> (a - b) * (a - b) = a * a + b * b - 2 * (a * b).
 Proof.
   intros a b H.
-rewrite <- (Nat.sub_add b a H); lia.
+  rewrite <- (Nat.sub_add b a H). lia.
 Qed.
 
 Lemma root_monotonic : forall x y : nat, x * x < y * y -> x < y.
@@ -41,24 +42,25 @@ apply (lt_monotonic_inverse (fun x => x * x)).
   apply Nat.square_lt_mono.
 Qed.
 
-(** The lia tactic easily proves simple arithmetic statements. *)
 Lemma square_recompose : forall x y : nat, x * y * (x * y) = x * x * (y * y).
 Proof. lia. Qed.
 
 (** ** Key arithmetic lemmas *)
 
 Section sqrt2_decrease.
+
   (** We use sections to simplify lemmas that use the same assumptions. *)
+
   Variables (p q : nat).
-Hypotheses (pos_q : 0 < q) (hyp_sqrt : p * p = 2 * (q * q)).
+  Hypotheses (pos_q : 0 <> q) (hyp_sqrt : p * p = 2 * (q * q)).
 
   Lemma sqrt_q_non_zero : 0 <> q * q.
   Proof. lia. Qed.
 
-(** We define a local custom proof tactic. *)
+  (** Define a local custom proof tactic. *)
   Local Ltac solve_comparison :=
     apply root_monotonic; repeat rewrite square_recompose; rewrite hyp_sqrt;
-   rewrite (Nat.mul_assoc _ 2 _); apply Nat.mul_lt_mono_pos_r;
+     rewrite (mult_assoc _ 2 _); apply Nat.mul_lt_mono_pos_r;
       auto using sqrt_q_non_zero with arith.
 
   Lemma comparison1 : q < p.
@@ -88,20 +90,21 @@ Qed.
 Lemma new_equality :
  (3 * p - 4 * q) * (3 * p - 4 * q) = 2 * ((3 * q - 2 * p) * (3 * q - 2 * p)).
 Proof.
-repeat rewrite sub_square_identity;
- auto using comparison2,comparison3 with arith.
+    rewrite! sub_square_identity.
+    all: auto using comparison2,comparison3 with arith.
     lia.
   Qed.
 
   (**
-After the section, lemmas inside the section are generalized
-with the variables and hypotheses they use.
+     After the `End` command, lemmas inside the section are generalized
+     with the variables and hypotheses they depend on.
    *)
 End sqrt2_decrease.
 
-(** ** Statement and proof *)
+(* The Main Action: Statement and Proof *)
 
-(** The proof proceeds by well-founded induction on q.
+(**
+   The proof proceeds by well-founded induction on q.
    We apply the induction hypothesis with the numbers <<3 * q - 2 * q>>
    and <<3 * p - 4 * q>>. This leaves two key proof goals:
    - <<3 * q - 2 * p <> 0>>, which we prove using arithmetic and the
@@ -110,13 +113,24 @@ and <<3 * p - 4 * q>>. This leaves two key proof goals:
      which we prove using the [new_equality] lemma above
  *)
 Theorem sqrt2_not_rational :
- forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
+  forall p q : nat, q <> 0 -> ¬ p ^ 2 = 2 * (q ^ 2).
 Proof.
-intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf).
-clear q; intros q Hrec p Hneq.
-generalize (proj1 (Nat.neq_0_lt_0 _) Hneq); intros Hlt_O_q Heq.
-apply (Hrec (3 * q - 2 * p) (comparison4 _ _ Hlt_O_q Heq) (3 * p - 4 * q)).
-- apply sym_not_equal; apply Nat.lt_neq; apply Nat.add_lt_mono_l with (2 * p).
-  rewrite <- plus_n_O, Nat.add_comm, Nat.sub_add; auto using Nat.lt_le_incl,comparison2.
-- apply new_equality; auto.
+  assert (forall x, x ^ 2 = x * x) as sq. simpl; lia.
+  intros p q; rewrite! sq; clear sq.
+  revert p.
+  induction q using (well_founded_ind lt_wf).
+  intros p Hneq.
+  
+  specialize H with (y := 3 * q - 2 * p) (p := 3 * p - 4 * q).
+  intros Heq.
+  
+  apply H.
+  - apply comparison4. all: auto.
+  - apply sym_not_equal. apply Nat.lt_neq.
+    eapply plus_lt_reg_l.
+    rewrite <- plus_n_O. rewrite <- le_plus_minus.
+    all: auto using comparison2, lt_le_weak.
+  - apply new_equality.
+    + lia.
+    + assumption.
 Qed.
\ No newline at end of file