diff options
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Reals/Raxioms.v | 9 | ||||
-rw-r--r-- | theories/Reals/Rbase.v | 25 |
2 files changed, 16 insertions, 18 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index a9c3f621d..38c423938 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -29,8 +29,8 @@ Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``. Hints Resolve Rplus_Ropp_r : real v62. (**********) -Axiom Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. -Hints Resolve Rplus_ne : real v62. +Axiom Rplus_Ol:(r:R)``0+r==r``. +Hints Resolve Rplus_Ol : real. (***********************************************************) (*s Multiplication *) @@ -48,10 +48,9 @@ Hints Resolve Rmult_assoc : real v62. Axiom Rinv_l:(r:R)``r<>0``->``(1/r)*r==1``. Hints Resolve Rinv_l : real. - (**********) -Axiom Rmult_ne:(r:R)``r*1==r``/\``1*r==r``. -Hints Resolve Rmult_ne : real v62. +Axiom Rmult_1l:(r:R)``1*r==r``. +Hints Resolve Rmult_1l : real. (**********) Axiom R1_neq_R0:``1<>0``. diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index f2f6cc2d7..1fb31101d 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -19,8 +19,8 @@ Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false). Symmetry; Apply Rplus_assoc. Exact Rmult_sym. Symmetry; Apply Rmult_assoc. - Intro; Apply (let (H1,H2)=(Rplus_ne n) in H2). - Intro; Apply (let (H1,H2)=(Rmult_ne n) in H2). + Intro; Apply Rplus_Ol. + Intro; Apply Rmult_1l. Exact Rplus_Ropp_r. Intros. Rewrite Rmult_sym. @@ -253,16 +253,15 @@ Save. (*s Addition *) (*********************************************************) -Lemma Rplus_Or:(r:R)``r+0==r``. -Intro; Ring. +Lemma Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. +Intro;Split;Ring. Save. -Hints Resolve Rplus_Or : real. +Hints Resolve Rplus_ne : real v62. -(**********) -Lemma Rplus_Ol:(r:R)``0+r==r``. +Lemma Rplus_Or:(r:R)``r+0==r``. Intro; Ring. Save. -Hints Resolve Rplus_Ol : real. +Hints Resolve Rplus_Or : real. (**********) Lemma Rplus_Ropp_l:(r:R)``(-r)+r==0``. @@ -335,16 +334,16 @@ Save. Hints Resolve Rmult_Ol : real v62. (**********) -Lemma Rmult_1r:(r:R)(``r*1==r``). -Intro; Ring. +Lemma Rmult_ne:(r:R)``r*1==r``/\``1*r==r``. +Intro;Split;Ring. Save. -Hints Resolve Rmult_1r : real. +Hints Resolve Rmult_ne : real v62. (**********) -Lemma Rmult_1l:(r:R)(``1*r==r``). +Lemma Rmult_1r:(r:R)(``r*1==r``). Intro; Ring. Save. -Hints Resolve Rmult_1l : real. +Hints Resolve Rmult_1r : real. (**********) Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``. |