1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 include "nat/plus.ma".
23 axiom Ropp:R→R. (*funzione da x → -x*)
30 interpretation "real plus" 'plus x y = (Rplus x y).
32 interpretation "real opp" 'uminus x = (Ropp x).
34 notation "hvbox(a break · b)"
35 right associative with precedence 55
38 interpretation "real mult" 'mult x y = (Rmult x y).
40 interpretation "real leq" 'leq x y = (Rle x y).
42 interpretation "real geq" 'geq x y = (Rge x y).
44 let rec elev (x:R) (n:nat) on n: R ≝
47 | S n ⇒ Rmult x (elev x n)
50 let rec real_of_nat (n:nat) : R ≝
56 | _ ⇒ real_of_nat n + R1
60 coercion cic:/matita/didactic/reals/real_of_nat.con.
62 axiom Rplus_commutative: ∀x,y:R. x+y = y+x.
63 axiom R0_neutral: ∀x:R. x+R0=x.
64 axiom Rdiv_le: ∀x,y:R. R1 ≤ y → Rdiv x y ≤ x.
65 axiom R2_1: R1 ≤ S (S O).
67 axiom Rmult_Rle: ∀x,y,z,w. x ≤ y → z ≤ w → Rmult x z ≤ Rmult y w.
69 axiom Rdiv_pos: ∀ x,y:R. R0 ≤ x → R1 ≤ y → R0 ≤ Rdiv x y.
70 axiom Rle_R0_R1: R0 ≤ R1.
71 axiom div: ∀x:R. x = Rdiv x (S (S O)) → x = O.
72 (* Proprieta' elevamento a potenza NATURALE *)
73 axiom elev_incr: ∀x:R.∀n:nat. R1 ≤ x → elev x (S n) ≥ elev x n.
74 axiom elev_decr: ∀x:R.∀n:nat. R0 ≤ x ∧ x ≤ R1 → elev x (S n) ≤ elev x n.
75 axiom Rle_to_Rge: ∀x,y:R. x ≤ y → y ≥ x.
76 axiom Rge_to_Rle: ∀x,y:R. x ≥ y → y ≤ x.
78 (* Proprieta' elevamento a potenza TRA REALI *)
80 axiom Relev_ge: ∀x,y:R.
81 (x ≥ R1 ∧ y ≥ R1) ∨ (x ≤ R1 ∧ y ≤ R1) → Relev x y ≥ x.
82 axiom Relev_le: ∀x,y:R.
83 (x ≥ R1 ∧ y ≤ R1) ∨ (x ≤ R1 ∧ y ≥ R1) → Relev x y ≤ x.
86 lemma stupido: ∀x:R.R0+x=x.
88 conclude (R0+x) = (x+R0).
93 axiom opposto1: ∀x:R. x + -x = R0.
94 axiom opposto2: ∀x:R. -x = Rmult x (-R1).
95 axiom meno_piu: Rmult (-R1) (-R1) = R1.
96 axiom R1_neutral: ∀x:R.Rmult R1 x = x.
98 axiom uffa: ∀x,y:R. R1 ≤ x → y ≤ x · y.