proposition: Lemma unzip2_rcons {S T : Type} (s : seq (S*T)) (h : S*T) : unzip2 (rcons s h) = rcons (unzip2 s) (snd h).
proof: Proof. elim: s => [ | h0 s IH] //= ; by rewrite IH. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)