proposition: Lemma AbsIR_sqrt_sqr : forall x x2pos, AbsIR x [=] sqrt (x[^]2) x2pos.
proof: Proof. intros x xxpos. unfold AbsIR in |- *. simpl in |- *. unfold ABSIR in |- *. apply equiv_imp_eq_max; intros. apply power_cancel_leEq with 2. auto. apply mult_cancel_leEq with (Two:IR). apply pos_two. rstepl (x[+][--]x). rstepr (y[+]y). apply plus_resp_leEq_both; auto. astepl ([1][*]x[*]x). rstepl (x[^]2[+][0]). apply shift_plus_leEq'. rstepr ((y[-]x) [*] (y[-][--]x)). apply mult_resp_nonneg. apply shift_zero_leEq_minus. auto. apply shift_zero_leEq_minus. auto. apply leEq_transitive with (sqrt (x[^]2) xxpos). apply power_cancel_leEq with 2. auto. apply sqrt_nonneg. astepr (x[^]2). apply leEq_reflexive. auto. apply leEq_transitive with (sqrt (x[^]2) xxpos). apply power_cancel_leEq with 2. auto. apply sqrt_nonneg. astepr (x[^]2). rstepl (x[^]2). apply leEq_reflexive. auto. Qed.
imports: CoRN.reals.OddPolyRootIR