proposition: Lemma AbsIR_recip : forall x x_ x__, AbsIR ([1][/] x[//]x_) [=] ([1][/] AbsIR x[//]x__).
proof: Proof. intros x H Ha. apply eq_transitive_unfolded with (AbsIR [1][/] AbsIR x[//]Ha). apply AbsIR_division. apply div_wd. 2: algebra. apply AbsIR_eq_x; apply less_leEq; apply pos_one. Qed.
imports: CoRN.reals.OddPolyRootIR