proposition: Lemma Exercise3_5a r f: orsum_ax r f -> cardinal (substrate (order_sum r f)) = csum (fam_card_sub f).
proof: Proof. move=> osa. rewrite orsum_sr // /sum_of_substrates /fam_card_sub . by apply:csum_pr3; aw; trivial => i idf; rewrite !LgV//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)