proposition: Lemma outside_square_10 : forall a b c d : Z, (outside_square a b c d < -2)%Z -> (d <= 0)%Z.
proof: Proof. intros [| pa| pa] [| pb| pb] [| pc| pc] [| pd| pd]; repeat rewrite Zplus_0_r; repeat rewrite Zplus_0_l; intro H; first [ intro H_discriminate_me; discriminate H_discriminate_me | discriminate H | repeat constructor | apply Zero_le_Qpos ]. Qed.
imports: Coq(ZArithRing)