proposition: Lemma productb_gr x: productb (Lg (domain x) (Vg x)) = productb x.
proof: Proof. set_extens t; move /setXb_P => [p1]; aw => p2 p3;apply /setXb_P; aw; split => // i idg; move: (p3 _ idg); rewrite LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)