proposition: Lemma length_list_drop: forall {T: Type} i (x: list T), i < Datatypes.length x -> Datatypes.length (list_drop i x) = Datatypes.length x - i.
proof: Proof. intros. generalize dependent i. induction x; destruct i; simpl; intros. { reflexivity. } { reflexivity. } { reflexivity. } { apply IHx. intuition. } Qed.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)