proposition: Theorem cross1_correct: forall p, In p cross1 <-> exists x, exists y, In x indexes /\ In y ref_list /\ p = (x, y).
proof: Proof. intros p; exact (in_fold_map _ (fun x y => (x, y)) p ref_list indexes). Qed.
imports: List UList Permutation Div OrderedList ListOp Lia