proposition: Lemma AbsIR_division : forall x y y_ y__, AbsIR (x[/] y[//]y_) [=] (AbsIR x[/] AbsIR y[//]y__).
proof: Proof. intros x y H Hy. rstepr (AbsIR x[*] ([1][/] AbsIR y[//]Hy)). apply eq_transitive_unfolded with (AbsIR (x[*] ([1][/] y[//]H))). apply un_op_wd_unfolded; rational. apply eq_transitive_unfolded with (AbsIR x[*]AbsIR ([1][/] y[//]H)). apply AbsIR_resp_mult. apply mult_wdr. cut (y [<] [0] or [0] [<] y). intros H0. elim H0. intros. apply eq_transitive_unfolded with ( [--] ([1][/] y[//]H)). apply AbsIR_eq_inv_x. rstepr ([0][/] [--]y[//]inv_resp_ap_zero _ _ H). apply shift_leEq_div. astepl ( [--]ZeroR). apply inv_resp_less; assumption. rstepl ( [--]OneR). astepr ( [--]ZeroR); apply inv_resp_leEq; apply less_leEq; apply pos_one. rstepl ([1][/] [--]y[//]inv_resp_ap_zero _ _ H). apply div_wd. algebra. apply eq_symmetric_unfolded; apply AbsIR_eq_inv_x. apply less_leEq; assumption. intros. apply eq_transitive_unfolded with ([1][/] y[//]H). apply AbsIR_eq_x. apply less_leEq; apply recip_resp_pos; assumption. apply div_wd; [ algebra | apply eq_symmetric_unfolded; apply AbsIR_eq_x; apply less_leEq; assumption ]. apply ap_imp_less. assumption. Qed.
imports: CoRN.reals.OddPolyRootIR