proposition: Lemma semLiftProd4SizeMonotonic A1 A2 A3 A4 B (f : A1 -> A2 -> A3 -> A4 -> B) (g1 : G A1) (g2 : G A2) (g3 : G A3) (g4 : G A4) `{@SizeMonotonic _ _ PG g1} `{@SizeMonotonic _ _ PG g2} `{@SizeMonotonic _ _ PG g3} `{@SizeMonotonic _ _ PG g4} : semProd (liftProd4 f g1 g2 g3 g4) <--> [set b : B | exists a1 a2 a3 a4, semProd g1 a1 /\ semProd g2 a2 /\ semProd g3 a3 /\ semProd g4 a4 /\ f a1 a2 a3 a4 = b].
proof: Proof. rewrite /semProd. setoid_rewrite semLiftProd4Size. move => b. split. - move => [s [_ [a1 [a2 [a3 [a4 [Ha1 [Ha2 [Ha3 [Ha4 Hb]]]]]]]]]]; subst. exists a1. exists a2. exists a3. exists a4. repeat split; exists s; (split; [reflexivity | eassumption ]). - move => [a1 [a2 [a3 [a4 [[s1 [_ Ha1]] [[s2 [_ Ha2]] [[s3 [_ Ha3]] [[s4 [_ Ha4]] Hb]]]]]]]]; subst. exists (max s1 (max s2 (max s3 s4))). split; first by []. exists a1. exists a2. exists a3. exists a4. repeat split; (eapply monotonic; last eassumption); lia. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)