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