proposition: Theorem Zsame_sign_imp : forall u v, (0 < u -> 0 <= v)%Z -> (0 < -u -> 0 <= -v)%Z -> (0 <= u * v)%Z.
proof: Proof. intros [|u|u] v Hp Hn. easy. apply Zmult_le_0_compat. easy. now apply Hp. replace (Zneg u * v)%Z with (Zpos u * (-v))%Z. apply Zmult_le_0_compat. easy. now apply Hn. rewrite <- Zopp_mult_distr_r. apply Zopp_mult_distr_l. Qed.
imports: Coq(ZArith Lia Zquot)