proposition: Lemma Zsgn_16 : forall x y : Z, Z.sgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}.
proof: Proof. intros [| p1 | p1] [| p2 | p2]; simpl in |- *; intro H; try discriminate H; [ left | right ]; repeat split. Qed.
imports: Coq(Lia)