proposition: Theorem Zsame_sign_trans : forall v u w, v <> Z0 -> (0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z.
proof: Proof. intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now elim Zv. Qed.
imports: Coq(ZArith Lia Zquot)