fix(S3): rewrite continuous_entropy_le_ln_bma proof for Coq 9.1.1

Three Coquelicot/Coq 9.1.1 incompatibilities in the existing §8 proof:

1. `change scal with Rmult / change plus with Rplus` left ring unable to
   recognise the goal as an R equation — replaced with assert+exact pattern
   to prove equalities at type R first, then bridge via definitional V=R.

2. `apply ex_RInt_plus` could not unify abstract V with R_NormedModule in
   apply mode — replaced with `exact (ex_RInt_plus ...)` which uses
   definitional equality.

3. `rewrite (RInt_ext _ _ Hext)` was passing the proof term as the third
   arg (a : R) — fixed to `rewrite (RInt_ext _ _ _ _ Hext)` for all four
   explicit args (f g a b) before the equality proof.

Suite remains 39/39 passing.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

proofs/canonical-proof-suite/S3_h_theorem_ndim.v

@@ -675,20 +675,29 @@ Proof.
        with (1 / (b - a) - f x) in Htl
       by (field; lra).
     exact Htl. }
-  (* 2. Integrability of both integrands. *)
+  (* 2. Integrability of both integrands.
+     Note: ex_RInt_ext and RInt_ext produce equality goals at type V
+     (the CompleteNormedModule), not plain R.  ring does not recognise
+     @eq V goals, so each pointwise equality is proved as @eq R via an
+     intermediate assert and closed with exact (definitional V = R). *)
   assert (Hh_int : ex_RInt (fun x => f x * (- ln (b - a) - ln (f x))) a b).
   { apply (ex_RInt_ext
       (fun x => (- ln (b - a)) * f x + (-1) * (f x * ln (f x)))).
-    - intros x _. ring.
-    - apply ex_RInt_plus.
-      + exact (ex_RInt_scal _ a b (- ln (b - a)) Hf_ex).
-      + exact (ex_RInt_scal _ a b (-1) flnf_int). }
+    - intros x _.
+      assert (HH : (- ln (b - a)) * f x + (-1) * (f x * ln (f x))
+                   = f x * (- ln (b - a) - ln (f x))) by ring.
+      exact HH.
+    - exact (ex_RInt_plus _ _ a b
+        (ex_RInt_scal _ a b (- ln (b - a)) Hf_ex)
+        (ex_RInt_scal _ a b (-1) flnf_int)). }
   assert (Hg_int : ex_RInt (fun x => 1 / (b - a) - f x) a b).
   { apply (ex_RInt_ext (fun x => 1 / (b - a) + (-1) * f x)).
-    - intros x _. ring.
-    - apply ex_RInt_plus.
-      + apply ex_RInt_const.
-      + exact (ex_RInt_scal _ a b (-1) Hf_ex). }
+    - intros x _.
+      assert (HH : 1 / (b - a) + (-1) * f x = 1 / (b - a) - f x) by ring.
+      exact HH.
+    - exact (ex_RInt_plus _ _ a b
+        (ex_RInt_const a b (1 / (b - a)))
+        (ex_RInt_scal _ a b (-1) Hf_ex)). }
   (* 3. Integral monotonicity: RInt h <= RInt g. *)
   pose proof (RInt_le
     (fun x => f x * (- ln (b - a) - ln (f x)))
@@ -700,8 +709,11 @@ Proof.
   {
     assert (Hext1 : forall x, Rmin a b < x < Rmax a b ->
       f x * (- ln (b - a) - ln (f x)) = (- ln (b - a)) * f x + (-1) * (f x * ln (f x))).
-    { intros x _. ring. }
-    rewrite (RInt_ext _ _ Hext1).
+    { intros x _.
+      assert (HH : f x * (- ln (b - a) - ln (f x))
+                   = (- ln (b - a)) * f x + (-1) * (f x * ln (f x))) by ring.
+      exact HH. }
+    rewrite (RInt_ext _ _ _ _ Hext1).
     etransitivity. {
       exact (RInt_plus
         (fun x => (- ln (b - a)) * f x)
@@ -723,8 +735,10 @@ Proof.
   {
     assert (Hext2 : forall x, Rmin a b < x < Rmax a b ->
       1 / (b - a) - f x = 1 / (b - a) + (-1) * f x).
-    { intros x _. ring. }
-    rewrite (RInt_ext _ _ Hext2).
+    { intros x _.
+      assert (HH : 1 / (b - a) - f x = 1 / (b - a) + (-1) * f x) by ring.
+      exact HH. }
+    rewrite (RInt_ext _ _ _ _ Hext2).
     assert (Hconst_int : ex_RInt (fun _ : R => 1 / (b - a)) a b).
     { apply ex_RInt_const. }
     etransitivity. {