proposition: Lemma outside_square_1 : forall a b c d : Z, (2 < outside_square a b c d)%Z -> (0 < a + b + c + d)%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 [ discriminate H | repeat constructor ]. Qed.
imports: Coq(ZArithRing)