Two lemmas that used to pass no more now pass again. Bug simply because every

tactic argument now requires less question marks :-(

diff --git a/helm/software/matita/dama/integration_algebras.ma b/helm/software/matita/dama/integration_algebras.ma
index 0339a088929b0b5b6850770930867bab35b2f009..06f85c73c786888eb05850231f93139d08aef834 100644 (file)
--- a/helm/software/matita/dama/integration_algebras.ma
+++ b/helm/software/matita/dama/integration_algebras.ma
@@ -247,25 +247,23 @@ definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
 interpretation "Ordered field lt" 'lt a b =
  (cic:/matita/integration_algebras/lt.con _ a b).
 
-(*incompleto
 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
 intros;
- generalize in match (of_plus_compat ? ? ? ? ? ? ? ? F ? ? (-x) H); intro;
- rewrite > (zero_neutral ? ? ? ? F) in H1;
- rewrite > (plus_comm  ? ? ?  ? F) in H1;
- rewrite > (opp_inverse ? ? ? ? F) in H1;
- 
+ generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
+ rewrite > zero_neutral in H1;
+ rewrite > plus_comm in H1;
+ rewrite > opp_inverse in H1;
  assumption.
-qed.*)
-
-axiom le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
-(* intros;
- generalize in match (of_plus_compat ? ? ? ? ? ? ? ? F ? ? (-x) H); intro;
- rewrite > (zero_neutral ? ? ? ? F) in H1;
- rewrite > (plus_comm ? ? ? ? F) in H1;
- rewrite > (opp_inverse ? ? ? ? F) in H1;
+qed.
+
+lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
+ intros;
+ generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
+ rewrite > zero_neutral in H1;
+ rewrite > plus_comm in H1;
+ rewrite > opp_inverse in H1;
  assumption.
-qed.*)
+qed.
 
 (*
 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.