proposition: Lemma AbsIR_resp_mult : forall x y, AbsIR (x[*]y) [=] AbsIR x[*]AbsIR y.
proof: Proof. intros. astepl (sqrt ((x[*]y) [^]2) (sqr_nonneg _ (x[*]y))). cut ([0] [<=] x[^]2[*]y[^]2). intro. astepl (sqrt (x[^]2[*]y[^]2) H). Step_final (sqrt (x[^]2) (sqr_nonneg _ x) [*]sqrt (y[^]2) (sqr_nonneg _ y)). apply mult_resp_nonneg; apply sqr_nonneg. Qed.
imports: CoRN.reals.OddPolyRootIR