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