Double-checking correctness of big O formulas found online I found the formulas below on a website of a New Zealand university. This is the solution part to a question on big O formulas and wether they are right or wrong, and I wanted to check if these are actually correct.

I specifically have doubts about the fourth staement

$5n+8n^2+100n^3 =O(n^4)$

This is assumed correct. Since we usually take the highest leading element, should it not be $O(n^3)$ as opposed to $O(n^4)$?
Are the other proofs correct?
 A: They are correct.  Anything that is $O(n^3)$ is also $O(n^4)$.
A: To avoid any misunderstanding and ambiguity I'll write fully here what I mean:
$$5n+8n^2+100n^3 \notin O(n^2 \log n)$$
To prove it's enough to consider reverse inequality:
$$5n+8n^2+100n^3 > n^3 > n^2 \log n \Leftrightarrow n> \log n$$
It's big difference between $f=O(g)$, which mean $f \in O(g)$, and $O(f)=O(g)$, which often is understand as $O(f) \subset O(g)$, but in all your general formulas, rules of sums and products, holds $O(f) \subset O(g) \land O(g) \subset O(f)$, so equality here behaves exactly as equality between sets. Some of proofs, for example, rule of summation, I wrote here Arithmetic rules for big O notation, little o notation and so on...
Now, for example, let's take transitivity. For simplicity I consider non negative functions. Strict definition is:
$$O(g) =  \left\lbrace f:\exists C > 0, \exists N \in \mathbb{N}, \forall n (n >  N \& n \in \mathbb{N}) (f(n) \leqslant C \cdot g(n)) \right\rbrace$$
Obviously, we have:
$$O(f) \subset O(g) \land O(g) \subset O(h) \Rightarrow O(f) \subset O(h)$$
Now, let's notice, that
$$f \in O(g) \Rightarrow O(f) \subset O(g)$$
So
$$f \in O(g) \land g \in O(h) \Rightarrow f \in O(h)$$
But $g \in O(f) \land h \in O(f)$ doesn't give information about $h$ and $g$ mutual comparison.
