proposition: Theorem in_indexes: forall i, In i indexes <-> i < size.
proof: Proof. intros i; unfold indexes. destruct (in_progression size 0 i). rewrite Nat.add_0_r in H; split; intros; destruct H; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia