proposition: Lemma firstn_firstn: forall l:list A, forall i j : nat, firstn i (firstn j l) = firstn (min i j) l.
proof: Proof. intro l; induction l as [|x xs Hl]. - intros. simpl. now rewrite ?firstn_nil. - intros [|i]; [easy|]. intros [|j]; [easy|]. cbn. f_equal. apply Hl. Qed.
imports: PeanoNat