proposition: Lemma NoDup_all_bounded_Zlength': forall i size, (0 <= i < size)%Z -> forall L, NoDup L -> (forall j, In j L -> 0 <= j < size /\ j <> i)%Z -> (Zlength L <= size - 1)%Z.
proof: Proof. intros ? ? ?. rewrite <- (Z2Nat.id size) in *; try lia. remember (Z.to_nat size) as size_n. clear Heqsize_n. induction size_n; intros. 1: lia. replace (Z.of_nat (S size_n) - 1)%Z with (Z.of_nat size_n) by lia. assert (i = Z.of_nat size_n \/ 0 <= i < Z.of_nat size_n)%Z by lia. destruct H2. subst i. apply NoDup_all_bounded_Zlength. lia. apply H0. intros. specialize (H1 _ H2). lia. destruct (in_dec Z.eq_dec (Z.of_nat size_n) L); [rename i0 into H3 | rename n into H3]. - apply in_split in H3. destruct H3 as [l1 [l2 ?]]. subst L. apply NoDup_remove in H0. destruct H0. assert (forall j, In j (l1 ++ l2) -> 0 <= j < Z.of_nat size_n /\ j <> i)%Z. { intros. assert (In j (l1 ++ Z.of_nat size_n :: l2)). { apply in_or_app. apply in_app_or in H4. destruct H4; auto. right. right. trivial. } specialize (H1 _ H5). assert (0 <= j < Z.of_nat size_n \/ j = Z.of_nat size_n)%Z by lia. destruct H6. lia. subst j. contradiction. } specialize (IHsize_n H2 (l1 ++ l2) H0 H4). rewrite Zlength_app in *. rewrite Zlength_cons. lia. - assert (forall j, In j L -> 0 <= j < Z.of_nat size_n /\ j <> i)%Z. { intros. specialize (H1 _ H4). assert (0 <= j < Z.of_nat size_n \/ j = Z.of_nat size_n)%Z by lia. destruct H5. lia. subst. contradiction. } specialize (IHsize_n H2 _ H0 H4). 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