proposition: Lemma Forall2_SizeMonotonic {A} x n (gs : list (G A)) l : (x <= n)%coq_nat -> gs \subset SizeMonotonic -> List.Forall2 (semProdSize^~ x) gs l -> List.Forall2 (semProdSize^~ n) gs l.
proof: Proof. intros. induction H1; auto. apply subconsset in H0. destruct H0; auto. constructor; auto. eapply H0; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)