(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/decl".
+
include "nat/times.ma".
include "nat/orders.ma".
+include "decl.ma".
+
inductive L (T:Type):Type:=
bottom: L T
|j: T → L T.
for @{ 'equiv $a $b }.
interpretation "uguaglianza parziale" 'equiv x y =
- (cic:/matita/test/decl/eq.ind#xpointer(1/1) _ x y).
+ (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
-coercion cic:/matita/test/decl/L.ind#xpointer(1/1/2).
+coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
lemma sim: ∀T:Type. ∀x,y:T. (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? x).
intros.
axiom Rge: L R→L R→Prop.
interpretation "real plus" 'plus x y =
- (cic:/matita/test/decl/Rplus.con x y).
+ (cic:/matita/tests/decl/Rplus.con x y).
interpretation "real leq" 'leq x y =
- (cic:/matita/test/decl/Rle.con x y).
+ (cic:/matita/tests/decl/Rle.con x y).
interpretation "real geq" 'geq x y =
- (cic:/matita/test/decl/Rge.con x y).
+ (cic:/matita/tests/decl/Rge.con x y).
let rec elev (x:L R) (n:nat) on n: L R ≝
match n with
| S n ⇒ real_of_nat n + (j ? R1)
].
-coercion cic:/matita/test/decl/real_of_nat.con.
+coercion cic:/matita/tests/decl/real_of_nat.con.
axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).
axiom Rdiv_pos: ∀ x,y:R.
(j ? R0) ≤ (j ? x) → (j ? R1) ≤ (j ? y) → (j ? R0) ≤ Rdiv (j ? x) (j ? y).
axiom Rle_R0_R1: (j ? R0) ≤ (j ? R1).
-axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.
\ No newline at end of file
+axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.