proposition: Lemma csum_trivial4 f a: csum (restr f (singleton a)) = cardinal (Vg f a).
proof: Proof. have <-: Vg (restr f (singleton a)) a = Vg f a by rewrite LgV; fprops. apply: csum_trivial1; rewrite restr_d //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)