proposition: Lemma cprod_trivial1 x f: domain f = singleton x -> cprod f = cardinal (Vg f x).
proof: Proof. move=> df; symmetry; apply /card_eqP. exists (product1_canon (Vg f x) x); split. - apply: setX1_canon_fb. - by rewrite /product1_canon; aw. - by rewrite/ product1_canon; aw;apply: setX1_pr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)