proposition: Lemma lower_bound_affine_base_interval_twice:forall a b c d x, -Qone<=x -> x<=Qone -> -Qabs (a*c) + -Qabs (a*d+c*b)+b*d <= (a*x+b)*(c*x+d).
proof: Proof. intros a b c d x Hxl Hxu. assert (Hxx0:=Qmult_mult_nonneg x). assert (Hxx1:=Qmult_mult_Qle_Qone_Qopp_Qone _ Hxl Hxu). stepr ((a*c)*(x*x)+(a*d+c*b)*x+b*d); [|ring]. repeat apply Qle_plus_plus; trivial. stepl (-Qabs (a*c)*Qone); [|ring]; apply Qle_trans with (-Qabs (a*c)*(x*x)); [ apply Qle_opp; repeat rewrite <- Qmult_Qopp_left; apply Qle_reg_mult_l_strong; trivial; rewrite Qopp_involutive; apply Qabs_nonneg | apply Qle_reg_mult_r_strong; trivial; apply Qabs_Qle_Qopp ]... apply Qle_trans with (-Qabs((a*d+c*b)*x)); [|apply Qabs_Qle_Qopp]; apply Qopp_Qle; rewrite Qabs_Qmult; stepr (Qabs(a*d+c*b)*Qone); [|ring]; apply Qle_reg_mult_l_strong; [apply Qabs_nonneg|]; apply Qabs_8; trivial... Qed.