cleanup of the eq_trans burdain

[helm.git] / helm / software / matita / dama / ordered_group.ma

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 5b0f0aa9b6c0c386b1c06ed3cb9184d1a6aeb320..d2f96fb5c7c03faf6fdb1b76774fd49dd8c86c14 100644 (file)
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -37,18 +37,6 @@ record ogroup : Type ≝ {
   exc_canc_plusr: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g
 }.
 
-notation > "'Ex'≪" non associative with precedence 50 for
- @{'excedencerewritel}.
- 
-interpretation "exc_rewl" 'excedencerewritel = 
- (cic:/matita/excedence/exc_rewl.con _ _ _).
-
-notation > "'Ex'≫" non associative with precedence 50 for
- @{'excedencerewriter}.
- 
-interpretation "exc_rewr" 'excedencerewriter = 
- (cic:/matita/excedence/exc_rewr.con _ _ _).
-
 lemma fexc_plusr: 
   ∀G:ogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z.
 intros 5 (G x y z L); apply (exc_canc_plusr ??? (-z));
@@ -196,6 +184,5 @@ apply (le_rewr ??? b (zero_neutral ??));
 assumption;
 qed.
 
-
   
   
\ No newline at end of file