proposition: Lemma order_prod_pr r r': order r -> order r' -> (order_prod2 r r') \Is (order_sum r' (cst_graph (substrate r') r)).
proof: Proof. move => or or'. have oa: (orsum_ax r' (cst_graph (substrate r') r)). by hnf; saw; hnf; aw;move=> i isr ;rewrite LgV. set fo:=order_sum r' (cst_graph (substrate r') r). have odf: order fo by rewrite /fo; fprops. move: (orsum_sr oa) => s1. move: (orprod2_or or or'). move: (orprod2_sr or or'). set io := order_prod2 r r'; move => s2 o2. pose f x := J (Vg x C1) (Vg x C0). have ta: (lf_axiom f (substrate io) (substrate fo)). move=> t; rewrite /fo s1 s2; move /setX2_P => [fgt dt va vb]. by apply: disjointU_pi; aw; trivial; rewrite !LgV//; aw. have bf: bijection (Lf f (substrate io) (substrate fo)). apply: lf_bijective =>//. move=> u v;rewrite s2 /f; move=> ud vd eq. move: (pr2_def eq)(pr1_def eq) => p1 p2. by apply: (setXf_exten ud vd); move=> i itp; try_lvariant itp. rewrite s1 /fam_of_substrates /cst_graph. move=> y ys; move:(du_index_pr1 ys); rewrite Lgd. move=> [Qsr]; rewrite LgV//; move=> Psr py. exists (variantLc (Q y) (P y)). rewrite s2; apply /setX2_P;split => //; aww. by symmetry;rewrite /f; aw. exists (Lf f (substrate io) (substrate fo));hnf; split => //. saw. hnf; aw; move=> x y xs ys; aw. move : (ta _ xs) (ta _ ys) => qa qb. have p1: inc (Vg x C0) (substrate r'). by move: xs; rewrite s2; move /setX2_P => [_ _ ]. apply (iff_trans (orprod2_gleP or or' _ _)); rewrite - s2. symmetry; apply (iff_trans (orsum_gleP _ _ _ _)). have ->: sum_of_substrates (cst_graph (substrate r') r) = substrate fo by aw. rewrite !LfV //. split; move => [_ _ xx]; split => //; move: xx; rewrite /f /order_sum_r !pr1_pair !pr2_pair !LgV //; case; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)