proposition: Lemma isum_p5 i j: glt r i j -> ipartial_sum (doubleton i j) = Vg f i +o Vg f j.
proof: Proof. move => lij. move: (arg1_sr (proj1 lij)) (arg2_sr (proj1 lij)) => iE jE. have h: (forall i0 j0, inc i0 (singleton i) -> inc j0 (singleton j) -> glt r i0 j0). by move => i0 j0 /set1_P -> /set1_P ->. move: (isum_p4 (set1_sub iE) (set1_sub jE) h). by rewrite (isum_p3 iE) (isum_p3 jE) setU2_11. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)