proposition: Lemma size_map2 s1 s2 : size (map2 s1 s2) = maxn (size s1) (size s2).
proof: Proof. elim: s1 s2 => [|x1 s1 IHs1] s2; elim: s2 => [|x2 s2 IHs2] //=. - by rewrite IHs2 !max0n. - by rewrite IHs1 maxnSS. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2