proposition: Lemma Forall2_cons T U (P : T -> U -> Prop) x1 s1 x2 s2 : List.Forall2 P (x1 :: s1) (x2 :: s2) <-> P x1 x2 /\ List.Forall2 P s1 s2.
proof: Proof. split=> [H|[? ?]]; last by constructor. by inversion H. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)