proposition: Lemma orsum_invariant2 r g g': order r -> substrate r = domain g -> substrate r = domain g' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' i)) -> (order_sum r g) \Is (order_sum r g').
proof: Proof. move=> or sr sr' ai. apply: (orsum_invariant1 (conj or sr) (conj or sr') (identity_is or)). move => i isr; rewrite idV //; apply: ai =>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)