proposition: Lemma nth_map2_dflt (n : nat) (s1 s2 : seq C) : nth x0 (map2 s1 s2) n = match size s1 <= n, size s2 <= n with | true, true => x0 | true, false => op' (nth x0 s2 n) | false, true => nth x0 s1 n | false, false => op (nth x0 s1 n) (nth x0 s2 n) end.
proof: Proof. elim: s1 s2 n => [|x1 s1 IHs1] s2 n. elim: s2 n => [|x2 s2 /= IHs2] n //=; first by rewrite nth_nil. by case: n =>[|n] //=; rewrite IHs2. case: s2 => [|x2 s2] /=. by case: leqP => H; last rewrite nth_default. case: n => [|n] /=. done. exact: IHs1. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2