proposition: Lemma oprod_pr1 a b r: ordinalp a -> ordinalp b -> (ordinal_o b) \Is r -> a *o b = osum r (cst_graph (substrate r) a).
proof: Proof. move=> ota otb ibr. have wo0:= (ordinal_o_wor ota). have wo1 := (ordinal_o_wor otb). have wo2:= (worder_invariance ibr wo1). rewrite /oprod2 /osum {1} /cst_graph. apply: ordinal_o_isu1. by apply: orprod2_wor; apply: ordinal_o_wor. apply: orsum_wor; first by aw. hnf; aw => i iser; rewrite !LgV //? Lgd //. apply: (orderIT (order_prod_pr (worder_or wo0)(worder_or wo1))). have [f isf] := ibr. rewrite /cst_graph; apply: (@orsum_invariant1 _ _ f); aw; trivial. - rewrite ordinal_o_sr; apply: sub_osr. - split; fprops. move: isf => [_ _ [[[ff _] _] <- tf] _] i id. move: (Vf_target ff id); rewrite tf=> vt; rewrite !LgV// ? Lgd //. apply: orderIR; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)