X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fordered_groups.ma;h=c9cab27f85e542b71265fd2244dfa9c9a1ecdce8;hb=ae98f5490e20dd26ece5804d9847acfba0e4d16b;hp=c9ef72c8ae4989ed600205ea88cf9dd29b5b6fe9;hpb=3f70fa72abe1d8453ea3565f4a33a05832dbc2e0;p=helm.git

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index c9ef72c8a..c9cab27f8 100644
--- a/matita/dama/ordered_groups.ma
+++ b/matita/dama/ordered_groups.ma
@@ -65,9 +65,9 @@ lemma le_zero_x_to_le_opp_x_zero:
 intros (G x Px);
 generalize in match (og_ordered_abelian_group_properties ? ? ? (-x) Px); intro;
 (* ma cazzo, qui bisogna rifare anche i gruppi con ≈ ? *)
- rewrite > zero_neutral in H1;
- rewrite > plus_comm in H1;
- rewrite > opp_inverse in H1;
+ rewrite > zero_neutral in H;
+ rewrite > plus_comm in H;
+ rewrite > opp_inverse in H;
  assumption.
 qed.