proposition: Lemma csum_trivial2 x f: domain f = singleton x -> cardinalp (Vg f x) -> csum f = Vg f x.
proof: Proof. by move=> df cV; rewrite (csum_trivial1 df) (card_card cV). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)