[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations

as suggested by @gares, and:

* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.

2 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out
index 8532b62a54..499d25391e 100644
--- a/test-suite/output/ssr_under.out
+++ b/test-suite/output/ssr_under.out
@@ -1,2 +1,4 @@
 'Under[ m - m ]
 (G (fun _ : nat => 0) n >= 0)
+'Under[ r = R0 \/ E r ]
+(Rbar_le Rbar0 (Lub_Rbar (fun r : R => r = R0 \/ E r)))
diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v
index b11dd1509c..7335c87e61 100644
--- a/test-suite/output/ssr_under.v
+++ b/test-suite/output/ssr_under.v
@@ -13,3 +13,18 @@ Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
 under eq_G => m do show; rewrite subnn.
 show.
 Abort.
+
+Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar).
+Parameter Rbar_le : Rbar -> Rbar -> Prop.
+Parameter Lub_Rbar : (R -> Prop) -> Rbar.
+Parameter Lub_Rbar_eqset :
+  forall E1 E2 : R -> Prop,
+    (forall x : R, E1 x <-> E2 x) ->
+    Lub_Rbar E1 = Lub_Rbar E2.
+
+Lemma test_Lub_Rbar (E : R -> Prop)  :
+  Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)).
+Proof.
+under Lub_Rbar_eqset => r do show.
+show.
+Abort.