proposition: Lemma OT_sum_invariant3 r g: order r -> substrate r = domain g -> order_fam g -> order_type_of (order_sum r g) = OT_sum r (Lg (substrate r) (fun i => order_type_of (Vg g i))).
proof: Proof. move => or sr alo. rewrite /OT_sum;apply: order_type_unique. apply: orsum_invariant2; fprops;aw; trivial. rewrite sr;move=> i isr ; rewrite !LgV//; move: (alo _ isr) => oi. by rewrite OT_prop4 //; apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)