I've read in different sources that the amortized cost of a red-black tree rebalancing is constant (at least during the tree creation using only insertions). How can it be proved?
If you look at the rules for what happens in a red/black tree insertion, you can see that the fixup rules for maintaining the red/black invariants only propagate upward if the newly-inserted node becomes the child of a red node with a red sibling.
Let's call a "fissionable" group in the red/black tree a black node with two red children. If you do an insertion into a fissionable group, the fissionable group will be recolored and rotated in a way that ends up eliminating that fissionable group, but which propagates the insertion fixup to a higher level in the tree. If you set the potential function of a red/black tree to be the number of fissionable groups in the tree, then the true cost of doing an insertion is 1 + r, where r is the number of groups destroyed, and the number of new fissionable groups created is at most one (you should check this), so the amortized cost of a fixup is O(1) because the potential drop is r.
It's a lot easier to think about this by looking at the isometry between red/black trees and 2-3-4 trees. A fissionable group in a red/black tree corresponds to a 4-node in a 2-3-4 tree, and if you understand 2-3-4 tree insertions it's pretty easy to see why the amortized cost of an insertion into a red/black tree is O(1).