proposition: Lemma semLiftProd2SizeMonotonic {A1 A2 B} (f: A1 -> A2 -> B) (g1 : G A1) (g2 : G A2) `{@SizeMonotonic _ _ PG g1} `{@SizeMonotonic _ _ PG g2} : semProd (liftM2 f g1 g2) <--> f @2: (semProd g1, semProd g2).
proof: Proof. rewrite /semProd. setoid_rewrite semLiftProd2Size. move => b. split. - move => [sb [_ Hb]]. destruct Hb as [a [[Hb11 Hb12] Hb2]]. exists a. split; [| by apply Hb2]. split; eexists; by split; [| eassumption]. - move => [[a1 a2] [[[s1 [_ G1]] [s2 [_ G2]]] Hf]]. compute in Hf. exists (max s1 s2). split; first by []. exists (a1,a2). split; last by []. split => /=; (eapply monotonic; last eassumption). lia. lia. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)