proposition: Lemma AbsIR_div_two : forall x, AbsIR (x [/]TwoNZ) [=] AbsIR x [/]TwoNZ.
proof: Proof. intros. apply eq_transitive_unfolded with (AbsIR x[/] AbsIR Two[//] AbsIR_resp_ap_zero _ (ap_symmetric_unfolded _ _ _ (less_imp_ap _ _ _ (pos_two _)))). apply AbsIR_division. apply div_wd. algebra. apply AbsIR_eq_x; apply less_leEq; apply pos_two. Qed.
imports: CoRN.reals.OddPolyRootIR