proposition: Lemma isum_p0 I: ipartial_sum I = ordinal (ipartial_order I).
proof: Proof. rewrite /ipartial_sum /ipartial_order /osum; f_equal; f_equal. by rewrite /Lgcomp; aw; apply: Lg_exten => t tE /=; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)