proposition: Lemma orprod_invariant2 r g g': worder r -> substrate r = domain g -> substrate r = domain g' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' i)) -> (order_prod r g) \Is (order_prod r g').
proof: Proof. move=> wor sr sr' alo. have or:=proj1 wor. apply: (orprod_invariant1 (conj wor sr) (conj or sr') (identity_is or)). by move=> i isr; rewrite idV //; apply: alo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)