proposition: Lemma directv_add_unique {U V} : reflect (forall u1 u2 v1 v2, u1 \in U -> u2 \in U -> v1 \in V -> v2 \in V -> (u1 + v1 == u2 + v2) = ((u1, v1) == (u2, v2))) (directv (U + V)).
proof: Proof. apply: (iffP directv_addP) => [dxUV u1 u2 v1 v2 Uu1 Uu2 Vv1 Vv2 | dxUV]. apply/idP/idP=> [| /eqP[-> ->] //]; rewrite -subr_eq0 opprD addrACA addr_eq0. move/eqP=> eq_uv; rewrite xpair_eqE -subr_eq0 eq_uv oppr_eq0 subr_eq0 andbb. by rewrite -subr_eq0 -memv0 -dxUV memv_cap -memvN -eq_uv !memvB. apply/eqP; rewrite -subv0; apply/subvP=> v /memv_capP[U1v U2v]. by rewrite memv0 -[v == 0]andbb {1}eq_sym -xpair_eqE -dxUV ?mem0v // addrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)