Prove "cross split" rule for Qp.

Terminology taken from "A Fresh Look at Separation Algebras and Share"
by Dockins et al.
7 jobs for master in 28 minutes and 12 seconds
Status Job ID Name Coverage
  Build
passed #10336
fp
build-coq.8.6.0

00:08:32

passed #10335
fp
build-coq.8.6.1

00:08:29

passed #10334
fp
build-coq.8.7.0

00:08:25

passed #10333
fp
build-coq.8.7.1

00:11:12

passed #10332
fp-timing
build-coq.8.7.2

00:08:39

passed #10331
fp
build-coq.8.8.dev

00:19:34

passed #10330
fp
build-coq.dev

00:19:34