DeriveInteriorProductFormula[(A⋀B)⊖X] derives the interior product formula for the expansion of (A⋀B)⊖X by repeated application of the first interior product formula. X may be a simple exterior product of 1-element factors, or it may be a numerically graded symbol, A and B can be arbitrary expressions, but A must be gradeable.