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