proposition: Lemma NoDup_all_bounded_Zlength: forall (size : Z), (0 <= size)%Z -> forall L, NoDup L -> (forall j, In j L -> 0 <= j < size)%Z -> (Zlength L <= size)%Z.
proof: Proof. intros ? ?. rename H into Ha. rewrite <- (Z2Nat.id size) in *; trivial. remember (Z.to_nat size) as size_n. clear Heqsize_n Ha. induction size_n; intros. - destruct L. + rewrite Zlength_nil. apply Nat2Z.is_nonneg. + exfalso. specialize (H0 z (in_eq _ _)). lia. - destruct (in_dec Z.eq_dec (Z.of_nat size_n) L); [rename i into H1 | rename n into H1]. + apply in_split in H1. destruct H1 as [l1 [l2 ?]]. subst L. apply NoDup_remove in H. destruct H. assert (forall j : Z, In j (l1 ++ l2) -> 0 <= j < Z.of_nat size_n)%Z. { intros. assert (In j (l1 ++ Z.of_nat size_n :: l2)). { apply in_or_app. apply in_app_or in H2. destruct H2; auto. right. right. trivial. } specialize (H0 _ H3). rewrite Nat2Z.inj_succ in H0. assert (0 <= j < Z.of_nat size_n \/ j = Z.of_nat size_n)%Z by lia. destruct H4; auto. subst j. contradiction. } specialize (IHsize_n (l1 ++ l2) H H2). rewrite Zlength_app in *. rewrite Zlength_cons. simpl. lia. + rewrite Nat2Z.inj_succ. assert (forall j, In j L -> 0 <= j < Z.of_nat size_n)%Z. { intros. specialize (H0 _ H2). rewrite Nat2Z.inj_succ in H0. assert (0 <= j < (Z.of_nat size_n) \/ j = (Z.of_nat size_n))%Z by lia. destruct H3; auto. subst. contradiction. } specialize (IHsize_n _ H H2). lia. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver