proposition: Lemma Forall_seqP {P : nat -> Prop} {m n: nat} : Forall P (seq m n) <-> (forall i, m <= i < m + n -> P i).
proof: Proof. rewrite Forall_forall. constructor; move=> H ? ?; apply H; by apply /in_seq. Qed.
imports: List Lia ssreflect ssrbool ssrfun