proposition: Lemma In_remove_length: forall {A: Type} (eq_dec : forall x y : A, {x = y} + {x <> y}) (l: list A) x, In x l -> length (remove eq_dec x l) < length l.
proof: Proof. intros ? ? l x. apply (@proj1 _ (length (remove eq_dec x l) <= length l)). induction l. + split; [intro H; inversion H | reflexivity]. + simpl. destruct (eq_dec x a). - split; [intros; lia | lia]. - split. * intros. simpl. destruct IHl. destruct H; [congruence | apply H0 in H]. lia. * simpl; 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