proposition: Theorem Zsame_sign_trans_weak : forall v u w, (v = Z0 -> w = 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 discriminate Zv. Qed.
imports: Coq(ZArith Lia Zquot)