proposition: Lemma Qhomographic_sign_dL_10 : forall (a b c d : Z) (p xs : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero (c + d) d xs) (H_Qhomographic_sg_denom_nonzero_dL : Qhomographic_sg_denom_nonzero c d (dL xs)), b <> 0%Z -> d <> 0%Z -> ~ inside_interval_1 (outside_interval a b) (outside_interval c d) -> ~ inside_interval_2 (outside_interval a b) (outside_interval c d) -> Qhomographic_sign a b c d (dL xs) H_Qhomographic_sg_denom_nonzero_dL = Qhomographic_sign (a + b) b (c + d) d xs H_Qhomographic_sg_denom_nonzero.
proof: Proof. intros; simpl in |- *; case (Z_zerop b); intro Hb; [ Falsum | case (Z_zerop d); intro Hd; [ Falsum | case (inside_interval_1_dec_inf (outside_interval a b) (outside_interval c d)); intro H_inside_1; [ Falsum | case (inside_interval_2_dec_inf (outside_interval a b) (outside_interval c d)); intro H_inside_2; [ Falsum | apply Qhomographic_sign_equal ] ] ] ]. Defined.
imports: Coq(ZArithRing)