proposition: Theorem cross2_correct: forall p, In p cross2 <-> valid_pos p.
proof: Proof. intros p; case (in_fold_map _ (fun x y => Pos x y) p indexes indexes). intros H1 H2; split; intros H3. case H1; auto. intros x (y, (U1, (U2, U3))). rewrite U3; split; auto. case (in_progression size 0 x); auto with arith. rewrite Nat.add_0_r; intros H _; case H; auto. case (in_progression size 0 y); auto with arith. rewrite Nat.add_0_r; intros H _; case H; auto. apply H2; clear H1 H2. generalize H3; case p; clear p H3; intros x y (H3, H4). exists x; exists y; repeat split; auto with arith. case (in_progression size 0 x); auto with arith. case (in_progression size 0 y); auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia