proposition: Lemma x_div_Max_leEq_x : forall x y : IR, [0] [<] x -> (x[/] Max y [1][//]max_one_ap_zero _) [<=] x.
proof: Proof. intros. apply shift_div_leEq'. apply pos_max_one. astepl ([1][*]x). apply mult_resp_leEq_rht; [ apply rht_leEq_Max | apply less_leEq; assumption ]. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq