proposition: Lemma Zsgn_20 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x + y < 0)%Z.
proof: Proof. Proof. intros [| p1 | p1] [| p2 | p2]; simpl in |- *; intro H; discriminate H || (constructor || apply Zsgn_11; assumption). Qed.
imports: Coq(Lia)