previously hidden simplifications (in old destruct) added

[helm.git] / matita / dama / ordered_groups.ma

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index c9ef72c8ae4989ed600205ea88cf9dd29b5b6fe9..c9cab27f85e542b71265fd2244dfa9c9a1ecdce8 100644 (file)
--- 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.