proposition: Lemma Exercise2_1d r: order r -> exists g h, [/\ order_fam g, (allf g total_order) & order_morphism h r (order_product g)].
proof: Proof. move=> or. move: (Exercise2_1c or);set bs := Zo _ _ => rp. set (g:= Lg bs id). have poa: order_fam g. rewrite /g;hnf; aw; move=> i ib; rewrite LgV//. by move: ib =>/Zo_P [_ [[oi _] _]]. set (h := Lf (cst_graph bs) (substrate r) (prod_of_substrates g)). exists g, h; split => //. by rewrite /g; hnf;aw; move=> i idg; rewrite LgV//; move: idg => /Zo_hi []. move: (order_total_extension or) => [x [tox sx rx]]. move: (tox)=> [ox _]. have xb: (inc x bs) by apply: Zo_i=> //; apply /ordersP. have ta: (lf_axiom (cst_graph bs) (substrate r) (prod_of_substrates g)). move=> y ysr; apply /setXf_P; rewrite /cst_graph /g !Lgd;split;fprops. move => j jb; rewrite !LgV//. by move: jb =>/Zo_P [] /ordersP [_ ->]. move: (order_product_osr poa) => [o1 s1]. rewrite /h; split => //. saw; [ by apply: lf_function | done ]. red;aw;move=> u v usr vsr; rewrite !LfV//; split. move => h1; apply /order_product_gleP;split;fprops. rewrite /g /cst_graph; aw; move=> i idg; rewrite !LgV//. by move: idg => /Zo_hi [_ ]; apply. move/order_product_gleP => [_ _]; rewrite /g/cst_graph;aw => h1. hnf;rewrite (Exercise2_1c or) -/bs; apply:setI_i; first by ex_tac. by move=> y yb; move: (h1 _ yb); rewrite ! LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)