proposition: Theorem IRsquare_o : forall yl yu zl zu : R, (yl <= 0)%R -> (0 <= yu)%R -> (zl <= 0)%R -> (yl * yl <= zu)%R -> (yu * yu <= zu)%R -> forall y : R, (yl <= y <= yu)%R -> (zl <= y * y <= zu)%R.
proof: Proof. intros yl yu zl zu Hy1 Hy2 Hzl Hzu1 Hzu2 y (Hyl,Hyu). split. fold (Rsqr y). apply Rle_trans with 0%R ; auto with real. case (Rlt_le_dec 0 y) ; intro H. generalize (Rlt_le _ _ H). clear H. intro H. apply Rle_trans with (yu * yu)%R ; auto with real. apply Rle_trans with (2 := Hzu1). apply Rle_trans with (y * yl)%R. exact (monotony_1n _ _ _ H Hyl). exact (monotony_2n _ _ _ Hy1 Hyl). Qed.
imports: Reals