make fractional_split truly forwards lemmas

As Upamanyu pointed out, these lemmas do seem to be using AsFractional backwards still.

But this opens some further questions:

• should we have a variant of fractional_merge that looks like Φ (q1 + q2) -∗ P1 ∗ P2?
• fractional_half still looks suspicious

These lemmas are barely used in our CId projects: a grep for fractional_(merge|split|half) has only 4 hits

coq-users/reloc/theories/logic/spec_ra.v
208:    iApply (fractional_half_2 with "Hl1 Hl2").

coq-users/examples/theories/hocap/concurrent_runners.v
265:      { iApply (fractional_split_2 with "Htoken Htoken2").
308:      { iApply (fractional_split_2 with "HINIT HINIT'").
320:        { iApply (fractional_split_2 with "HSETRES HSETRES'").