proposition: Lemma Forall_repeatI {X : Type} {P : X -> Prop} {x n} : P x -> Forall P (repeat x n).
proof: Proof. elim: n; first by constructor. move=> ? IH ?. constructor; [done | by apply: IH]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun