(* $Id: Spec_CReals45.v,v 1.4 2000/10/11 08:50:10 janz Exp $ *) Fixpoint nreal [_R:Set; _zero,_one:_R; _add:_R->_R->_R; m:nat]: _R := Cases m of O => _zero | (S n) => (_add (nreal _R _zero _one _add n) _one) end. Definition cauchy [_R:Set; _zero:_R; _add:_R->_R->_R; _less:_R->_R->Prop; g:nat->_R]: Prop := (e:_R)(_less _zero e)-> (Ex [n:nat](m:nat)(le n m)-> ((_less (g m) (_add (g n) e))/\(_less (g n) (_add (g m) e)))). Record CReals45 : Type := { _R : Set; _is : _R->_R->Prop; _ap : _R->_R->Prop; _ap_irr : (x:_R)~(_ap x x); _ap_sym : (x,y:_R)(_ap x y)->(_ap y x); _ap_cot : (x,y:_R)(_ap x y)->(z:_R)(_ap x z)\/(_ap z y); _ap_tight : (x,y:_R)~(_ap x y)<->(_is x y); _zero : _R; _add : _R->_R->_R; _add_wd : (x1,x2,y1,y2:_R)(_is x1 x2)->(_is y1 y2)-> (_is (_add x1 y1) (_add x2 y2)); _add_strext : (x1,x2,y1,y2:_R)(_ap (_add x1 y1) (_add x2 y2))-> (_ap x1 x2)\/(_ap y1 y2); _add_assoc : (x,y,z:_R)(_is (_add x (_add y z)) (_add (_add x y) z)); _add_runit : (x:_R)(_is (_add x _zero) x); _add_commut : (x,y:_R)(_is (_add x y) (_add y x)); _minus : _R->_R; _minus_wd : (x,y:_R)(_is x y)->(_is (_minus x) (_minus y)); _minus_strext : (x,y:_R)(_ap (_minus x) (_minus y))->(_ap x y); _minus_proof : (x:_R)(_is (_add x (_minus x)) _zero); _one : _R; _times : _R->_R->_R; _times_wd : (x1,x2,y1,y2:_R)(_is x1 x2)->(_is y1 y2)-> (_is (_times x1 y1) (_times x2 y2)); _times_strext : (x1,x2,y1,y2:_R) (_ap (_times x1 y1) (_times x2 y2))-> (_ap x1 x2)\/(_ap y1 y2); _times_assoc : (x,y,z:_R) (_is (_times x (_times y z)) (_times (_times x y) z)); _times_runit : (x:_R)(_is (_times x _one) x); _times_commut : (x,y:_R)(_is (_times x y) (_times y x)); _dist : (x,y,z:_R)(_is (_times x (_add y z)) (_add (_times x y) (_times x z))); _non_triv : (_ap _one _zero); _rcpcl : (x:_R)(_ap x _zero)->_R; _rcpcl_ap_zero : (x:_R)(nzx:(_ap x _zero))(_ap (_rcpcl x nzx) _zero); _rcpcl_wd : (x:_R)(nzx:(_ap x _zero))(y:_R)(nzy:(_ap y _zero)) (_is x y)->(_is (_rcpcl x nzx) (_rcpcl y nzy)); _rcpcl_strext : (x:_R)(nzx:(_ap x _zero))(y:_R)(nzy:(_ap y _zero)) (_ap (_rcpcl x nzx) (_rcpcl y nzy))->(_ap x y); _rcpcl_proof : (x:_R)(nzx:(_ap x _zero)) (_is (_times x (_rcpcl x nzx)) _one); _less : _R->_R->Prop; _less_wdr : (x,y,z:_R)(_less x y)->(_is y z)->(_less x z); _less_wdl : (x,y,z:_R)(_less x y)->(_is x z)->(_less z y); _less_strext : (x1,x2,y1,y2:_R) (_less x1 y1)->(_less x2 y2)\/(_ap x1 x2)\/(_ap y1 y2); _less_trans : (x,y,z:_R)(_less x y)->(_less y z)->(_less x z); _less_irr : (x:_R)~(_less x x); _less_asym : (x,y:_R)(_less x y)->~(_less y x); _add_resp_less : (x,y:_R)(_less x y)-> (z:_R)(_less (_add x z) (_add y z)); _times_resp_pos : (x,y:_R)(_less _zero x)->(_less _zero y)-> (_less _zero (_times x y)); _less_conf_ap : (x,y:_R)(_ap x y)<->((_less x y)\/(_less y x)); _lim : (g:nat->_R)(cauchy _R _zero _add _less g)->_R; _lim_proof : (g:nat->_R)(c:(cauchy _R _zero _add _less g)) (e:_R)(_less _zero e)-> (Ex [n:nat](m:nat)(le n m)-> ((_less (g m) (_add (_lim g c) e)) /\(_less (_lim g c) (_add (g m) e)))); _arch_proof : (x:_R)(Ex [n:nat] (_less x (nreal _R _zero _one _add n))) }.