length_remove@{i|} {A : Type@{i}} (n : nat) (l : list A) (H : (n < length l)%nat) : length (remove n l) = nat_pred (length l)%nat. Proof. unfold remove. rewrite length_app@{i}. rewrite length_take. rewrite length_drop. rewrite nat_min_l. 2: exact (leq_trans _ H). rewrite <- nat_sub_l_add_r. 2: exact _. lhs nrapply nat_sub_succ_r. apply ap. apply nat_add_sub_cancel_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum