proposition: Lemma semSequenceProdSizeMonotonic A (gs : list (G A)) : (gs \subset SizeMonotonic) -> semProd (sequenceProd gs) <--> [set l | length l = length gs /\ List.Forall2 semProd gs l].
proof: Proof. intros. rewrite /semProd. setoid_rewrite semSequenceProdSize. move => l. split. - move => [n [ _ [H1 H2]]]. split; auto. induction H2; subst; simpl; constructor. + exists n. split; auto. reflexivity. + apply IHForall2; eauto. apply subconsset in H. destruct H; auto. - move => [H1 H2]. revert gs H H1 H2. induction l; intros gs H H1 H2. + destruct gs; try discriminate. exists 0. split; auto. reflexivity. + destruct gs; try discriminate. apply subconsset in H. move : H => [H3 H4]. inversion H2; subst. destruct H6 as [n [ _ H5]]. eapply IHl in H8; auto. destruct H8 as [x [_ [H7 H8]]]. destruct (le_dec x n) eqn:Hle. { exists n. split; eauto; first by reflexivity. split; auto. constructor; auto. eapply Forall2_SizeMonotonic; eauto. } { exists x. split; first by reflexivity. split; auto. constructor; auto. eapply H3; last by eassumption. lia. } Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)