proposition: Lemma isum_p2: ipartial_sum emptyset = \0o.
proof: Proof. apply: ordinal0_pr1; rewrite orsum_sr. apply/set0_P => t /disjointU_P/proj31; rewrite /fam_of_substrates !Lgd. by move/in_set0. hnf; move: (isum_q1 (@sub0_set E)) =>[[or _] ->];saw. by hnf; aw => i /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)