A failing unification of a coercion vs a term is now tried again after

[helm.git] / helm / matita / library / algebra / monoids.ma

diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma
index 7c40db1fd89bffad6aefb0b284c01f10e4f1b169..cf1e531f47c01b90e2633caa00952fc71f76fb42 100644 (file)
--- a/helm/matita/library/algebra/monoids.ma
+++ b/helm/matita/library/algebra/monoids.ma
@@ -51,12 +51,12 @@ interpretation "Semigroup coercion" 'semigroup M =
 definition is_left_inverse ≝
  λM:Monoid.
   λopp: M → M.
-   ∀x:M. op M (opp x) x = 1.
+   ∀x:M. (opp x)·x = 1.
    
 definition is_right_inverse ≝
  λM:Monoid.
   λopp: M → M.
-   ∀x:M. op M x (opp x) = 1.
+   ∀x:M. x·(opp x) = 1.
 
 theorem is_left_inverse_to_is_right_inverse_to_eq:
  ∀M:Monoid. ∀l,r.
@@ -64,7 +64,7 @@ theorem is_left_inverse_to_is_right_inverse_to_eq:
    ∀x:M. l x = r x.
  intros;
  generalize in match (H x); intro;
- generalize in match (eq_f ? ? (λy. op M y (r x)) ? ? H2);
+ generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
  simplify; fold simplify (op M);
  intro; clear H2;
  generalize in match (semigroup_properties M);