From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 25 Oct 2006 09:28:11 +0000 (+0000)
Subject: Two lemmas that used to pass no more now pass again. Bug simply because every
X-Git-Tag: 0.4.95@7852~855
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8782ac2a08fa0308be55bb1338bb4f632b4fb541;p=helm.git

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/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma
index 0339a0889..06f85c73c 100644
--- a/matita/dama/integration_algebras.ma
+++ b/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.