Paired forward NTTFast correctness

Correctness proof for running the paired radix-4 DIF stage loop as two independent transforms.

theorem CompPoly.CPolynomial.NTTFast.Plan.runStagesDIFRadix4PairWithTwiddles_eq_pair {R : Type u_1} [Field R] (D : NTT.Domain R) (a b : Array R) : runStagesDIFRadix4PairWithTwiddles D (twiddleTable D) (NTT.loadNaturalArray D a) (NTT.loadNaturalArray D b) = (runStagesDIFRadix4WithTwiddles D (twiddleTable D) (NTT.loadNaturalArray D a), runStagesDIFRadix4WithTwiddles D (twiddleTable D) (NTT.loadNaturalArray D b))

The paired radix-4 DIF stage loop is extensionally two independent stage loops.