proposition: Lemma sup_in_product_aux g A (f := fam_of_substrates g) (Ai:= fun i => (Vfs (pr_i f i) A)): order_fam g -> sub A (productb f) -> forall i, inc i (domain g) -> sub (Ai i) (substrate (Vg g i)).
proof: Proof. move=> Ha Hb i id. have dfdg: domain f = domain g by rewrite /f /fam_of_substrates; aw. have ->: substrate (Vg g i) = Vg f i by rewrite LgV. have Hc: sub A (source (pr_i f i)) by rewrite /pr_i; aw. have He: function (pr_i f i) by apply: pri_f => //; ue. move=> t /(Vf_image_P He Hc) [u uA ->]. have ->: (Vg f i = target (pr_i f i)) by rewrite /pr_i; aw. Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)