proposition: Lemma Exercise3_5d r f h: orprod_ax r f -> h \Is (order_prod r f) -> cardinal (substrate h) = cprod (fam_card_sub f).
proof: Proof. move=> oa [g [o1 o2 [bg sg tg] _]]. by rewrite - (Exercise3_5b oa) - sg - tg; apply /card_eqP; exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)