proposition: Lemma removelast_firstn : forall n l, n < length l -> removelast (firstn (S n) l) = firstn n l.
proof: Proof. intro n; induction n as [|n IHn]; intros [|? l]; [easy ..|]. cbn [length firstn]. destruct l. - now intros ? %Nat.succ_lt_mono. - now intros <- %Nat.succ_lt_mono %IHn. Qed.
imports: PeanoNat