proposition: Lemma outside_square_correct_1 : forall (a b c d : Z) (p1 p2 : Qpositive), (2 < outside_square a b c d)%Z -> ~ (b = 0%Z /\ c = 0%Z /\ d = 0%Z) -> Qlt Zero (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d).
proof: Proof. intros a b c d p1 p2 H_o2_gt_2 Hbcd; generalize (outside_square_3 _ _ _ _ H_o2_gt_2) (outside_square_4 _ _ _ _ H_o2_gt_2) (outside_square_5 _ _ _ _ H_o2_gt_2) (outside_square_6 _ _ _ _ H_o2_gt_2); intros Ha Hb Hc Hd; generalize (triple_not_equal_zero _ _ _ Hbcd); intros [H_| [H_| H_]]; match goal with | id1:(?X1 <> 0%Z),id2:(0 <= ?X1)%Z |- _ => generalize (Zle_neq_Zlt 0 X1 id2 id1); intro H_lt end. abstract (apply Qlt_le_reg_pos; [ apply Qlt_le_reg_pos; [ apply Qle_lt_reg_pos; [ idtac | apply Qlt_mult_pos_pos ] | idtac ] | idtac ]; try (repeat apply Qle_mult_nonneg_nonneg; try auto with *); replace Zero with (Z_to_Q 0); trivial; apply Z_to_Qle || apply Z_to_Qlt; assumption). abstract (apply Qlt_le_reg_pos; [ apply Qle_lt_reg_pos; [ idtac | apply Qlt_mult_pos_pos; try auto with * ] | idtac ]; try apply Qle_plus_pos_pos; try (repeat apply Qle_mult_nonneg_nonneg; try auto with *); replace Zero with (Z_to_Q 0); trivial; apply Z_to_Qle || apply Z_to_Qlt; assumption). abstract (apply Qle_lt_reg_pos; try repeat apply Qle_plus_pos_pos; try (repeat apply Qle_mult_nonneg_nonneg; try auto with *); replace Zero with (Z_to_Q 0); trivial; apply Z_to_Qle || apply Z_to_Qlt; assumption). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)