proposition: Lemma finprodUnE (f1 f2 : forall t, Us t) : finprod f1 \+ finprod f2 = finprod (fun t => f1 t \+ f2 t).
proof: Proof. by apply: fin_ext=>a; rewrite !sel_fin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)