Gauss lemma: primitive factorisations over $\mathbb Q$ can be cleared to primitive factorisations over $\mathbb Z$

By [L2], choose an integer numerator and nonzero integer denominator for each of the finitely many coefficients of $g$ and $h$. Their denominator products are nonzero by [L4] and are common denominators, so [L3] and division by the positive contents of the cleared polynomials give $g=rG$ and $h=sH$ with $r,s\in\mathbb Q^\times$ and primitive $G,H\in\mathbb Z[x]$ of the same positive degrees as $g,h$.

The equality $f=rsGH$, after writing $rs=a/b$ in lowest terms with $b>0$, gives $bf=aGH$; [L1] makes both $f$ and $GH$ primitive, so content multiplicativity gives $b=|a|$ and therefore $a/b=\pm1$; hence $f=\pm GH$.

Any integer factorization of a primitive polynomial into two nonunits has both factors of positive degree: a nonunit constant factor would have content greater than $1$, contradicting [L1]. Conversely, steps 1.1 and 2.1 turn every rational positive-degree factorization into an integer one. By [L5], irreducibility over the two rings is therefore equivalent for primitive positive-degree polynomials.