proposition: Lemma OT_sum_ordertype r g: order r -> substrate r = domain g -> order_fam g -> order_type (OT_sum r g).
proof: Proof. move=> or sr alo; apply: OT_prop1. apply: orsum_or; split => //; aw; trivial. by hnf; aw; move=> i idg; rewrite LgV//; apply: OT_prop3; apply: alo. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)