proposition: Lemma Exercise3_5b r f: orprod_ax r f -> cardinal (substrate (order_prod r f)) = cprod (fam_card_sub f).
proof: Proof. move=> rosa. rewrite orprod_sr // /prod_of_substrates /fam_card_sub -/(cprod _). rewrite 2! cprod_pr; aw;apply: cprodb_exten => i idf /=. by rewrite !LgV//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)