proposition: Lemma Qquadratic_sg_denom_nonzero_always : forall (k e f g h : Z) (p1 p2 : Qpositive), k <> 0%Z -> (0 < e)%Z -> (0 < f)%Z -> (0 < g)%Z -> (0 < h)%Z -> Qquadratic_sg_denom_nonzero (k * e) (k * f) (k * g) (k * h) p1 p2.
proof: Proof. intros k e f g h p1 p2 Hk He Hf Hg Hh. generalize e f g h He Hf Hg Hh p2. induction p1. intros. case p0. intros. apply Qquadratic_signok1. replace (k * e0 + k * f0 + k * g0 + k * h0)%Z with (k * (e0 + f0 + g0 + h0))%Z; try replace (k * e0 + k * f0)%Z with (k * (e0 + f0))%Z; try replace (k * e0 + k * g0)%Z with (k * (e0 + g0))%Z; try apply IHp1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. intros. apply Qquadratic_signok2. replace (k * e0 + k * f0 + k * g0 + k * h0)%Z with (k * (e0 + f0 + g0 + h0))%Z; try replace (k * e0 + k * f0)%Z with (k * (e0 + f0))%Z; try replace (k * f0 + k * h0)%Z with (k * (f0 + h0))%Z; try apply IHp1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. apply Qquadratic_signok0. reflexivity. replace (k * e0 + k * f0)%Z with ((e0 + f0) * k)%Z; try replace (k * g0 + k * h0)%Z with ((g0 + h0) * k)%Z; try apply Qhomographic_sg_denom_nonzero_always_1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. intros. case p0. intros. apply Qquadratic_signok3. replace (k * e0 + k * f0 + k * g0 + k * h0)%Z with (k * (e0 + f0 + g0 + h0))%Z; try replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z; try replace (k * e0 + k * g0)%Z with (k * (e0 + g0))%Z; try apply IHp1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. intros. apply Qquadratic_signok4. replace (k * e0 + k * f0 + k * g0 + k * h0)%Z with (k * (e0 + f0 + g0 + h0))%Z; try replace (k * g0 + k * h0)%Z with (k * (g0 + h0))%Z; try replace (k * f0 + k * h0)%Z with (k * (f0 + h0))%Z; try apply IHp1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. apply Qquadratic_signok0. reflexivity. replace (k * e0 + k * f0)%Z with ((e0 + f0) * k)%Z; try replace (k * g0 + k * h0)%Z with ((g0 + h0) * k)%Z; try apply Qhomographic_sg_denom_nonzero_always_1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. intros. apply Qquadratic_signok0'. reflexivity. replace (k * e0 + k * g0)%Z with ((e0 + g0) * k)%Z; try replace (k * f0 + k * h0)%Z with ((f0 + h0) * k)%Z; try apply Qhomographic_sg_denom_nonzero_always_1; try first [ assumption | repeat apply Zlt_resp_pos ]; try assumption; repeat match goal with | |- (?X1 = ?X2) => abstract ring end. Defined.
imports: QArithSternBrocot(general_Q Zaux)