Verify 馃悊 Tx_rollup_l2_qty.v
Verify the admitted lemmas in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/tx_rollup_l2_qty These admitted lemmas are added by https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/merge_requests/442 Similar proofs are given in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/saturation_repr or https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/tez_repr/