axiom Rle: R→R→Prop.
axiom Rge: R→R→Prop.
-interpretation "real plus" 'plus x y =
- (cic:/matita/didactic/reals/Rplus.con x y).
+interpretation "real plus" 'plus x y = (Rplus x y).
-interpretation "real opp" 'uminus x =
- (cic:/matita/didactic/reals/Ropp.con x).
+interpretation "real opp" 'uminus x = (Ropp x).
notation "hvbox(a break · b)"
right associative with precedence 55
for @{ 'mult $a $b }.
-interpretation "real mult" 'mult x y =
- (cic:/matita/didactic/reals/Rmult.con x y).
+interpretation "real mult" 'mult x y = (Rmult x y).
-interpretation "real leq" 'leq x y =
- (cic:/matita/didactic/reals/Rle.con x y).
+interpretation "real leq" 'leq x y = (Rle x y).
-interpretation "real geq" 'geq x y =
- (cic:/matita/didactic/reals/Rge.con x y).
+interpretation "real geq" 'geq x y = (Rge x y).
let rec elev (x:R) (n:nat) on n: R ≝
match n with