proposition: Lemma OT_prod_pr1 a b c: order_type a -> order_type b -> worder c -> b \Is c -> a *t b = OT_sum c (cst_graph (substrate c) a).
proof: Proof. move=> ota otb woc ibc. rewrite /OT_prod2 /OT_sum. have ora: order a by apply: OT_prop2. have orb: order b by apply: OT_prop2. move: (proj1 woc) => oc. apply: order_type_unique. have ->: domain (cst_graph (substrate c) a) = substrate c. by rewrite /cst_graph; aw. apply: (@orderIT (order_prod2 a b)). by apply: orprod_invariant4; apply: OT_prop0. move: (order_prod_pr ora orb);set aux := order_sum _ _ ; move=> h. apply: (@orderIT aux) => //. move: ibc => [f isf]. rewrite /aux /cst_graph; apply: (orsum_invariant1(f:=f)); aw => //. move: isf => [_ _ [[[ff _] _] sf tf] _]. rewrite - sf; move=> i id. move: (Vf_target ff id); rewrite -tf=> vt. by rewrite ! LgV// ; apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)