X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fexcess.ma;h=d8cf097668382310eb8eda47d9c382a72c04d0aa;hb=43b9e1971e142d55eea8ceb57d8e6ee6d83d3791;hp=061d2db9be34c33904e89ffad0b9cdfa634af351;hpb=ff19936bfb1e58fea074f71526b4cb7f410d81de;p=helm.git

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 061d2db9b..d8cf09766 100644
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -146,22 +146,22 @@ intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
 intro Xyz; apply Exy; apply unfold_apart; right; assumption;
 qed.
 
-notation > "'Ex'≪" non associative with precedence 50 for
- @{'excessrewritel}.
- 
-interpretation "exc_rewl" 'excessrewritel = 
- (cic:/matita/excess/exc_rewl.con _ _ _).
-
 lemma le_rewr: ∀E:excess.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
 intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
 intro Xyz; apply Exy; apply unfold_apart; left; assumption;
 qed.
 
-notation > "'Ex'≫" non associative with precedence 50 for
- @{'excessrewriter}.
+notation > "'Le'≪" non associative with precedence 50 for
+ @{'lerewritel}.
  
-interpretation "exc_rewr" 'excessrewriter = 
- (cic:/matita/excess/exc_rewr.con _ _ _).
+interpretation "le_rewl" 'lerewritel = 
+ (cic:/matita/excess/le_rewl.con _ _ _).
+
+notation > "'Le'≫" non associative with precedence 50 for
+ @{'lerewriter}.
+ 
+interpretation "le_rewr" 'lerewriter = 
+ (cic:/matita/excess/le_rewr.con _ _ _).
 
 lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
 intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
@@ -183,6 +183,18 @@ intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption]
 elim (Exy); left; assumption;
 qed.
 
+notation > "'Ex'≪" non associative with precedence 50 for
+ @{'excessrewritel}.
+ 
+interpretation "exc_rewl" 'excessrewritel = 
+ (cic:/matita/excess/exc_rewl.con _ _ _).
+
+notation > "'Ex'≫" non associative with precedence 50 for
+ @{'excessrewriter}.
+ 
+interpretation "exc_rewr" 'excessrewriter = 
+ (cic:/matita/excess/exc_rewr.con _ _ _).
+
 lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x.
 intros (A x y z E H); split; elim H; 
 [apply (le_rewr ???? (eq_sym ??? E));|apply (ap_rewr ???? E)] assumption;
@@ -193,6 +205,18 @@ intros (A x y z E H); split; elim H;
 [apply (le_rewl ???? (eq_sym ??? E));| apply (ap_rewl ???? E);] assumption;
 qed.
 
+notation > "'Lt'≪" non associative with precedence 50 for
+ @{'ltrewritel}.
+ 
+interpretation "lt_rewl" 'ltrewritel = 
+ (cic:/matita/excess/lt_rewl.con _ _ _).
+
+notation > "'Lt'≫" non associative with precedence 50 for
+ @{'ltrewriter}.
+ 
+interpretation "lt_rewr" 'ltrewriter = 
+ (cic:/matita/excess/lt_rewr.con _ _ _).
+
 lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
 intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
 whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)]