proposition: Lemma Exercise4_10b r n: order r -> natp n -> n <> \0c -> Ex4_10_conc r n -> Ex4_10_hyp r n.
proof: Proof. move => or nN nz [g [og altg cdg ssr rb]]. case: (emptyset_dichot (domain g)) => nedg. by case: nz; rewrite - cdg nedg cardinal_set0. set E := substrate r. pose f := cst_graph (domain g). set A := fun_image E f. set ff:= Lf f E A. have ta: lf_axiom f E A by rewrite /A;move => t tdg; apply /funI_P; ex_tac. have bf: bijection ff. apply: lf_bijective => //. move => u v udg vdg sv. move: (nedg) => [k kdg]; move: (f_equal (Vg^~ k) sv). rewrite /f/cst_graph ! LgV//. by move => y /funI_P. move:(order_product_osr og) => [or1 sr1]. have srA: sub A (substrate (order_product g)). have aux: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops. rewrite sr1. move => t /funI_P [z zi ->]; rewrite /f/cst_graph; aw. apply /prod_of_substratesP;split;aww. by move => i idg; rewrite LgV//; rewrite ssr. exists g, A, ff;split => //. move: (iorder_osr or1 srA) => [pa' pb']. rewrite /ff; split => //; first by rewrite pb'; saw. hnf; aw;move => x y xE yE. move: srA ;rewrite sr1 => srA. move:(ta _ xE) (ta _ yE) => xA yA. move: (srA _ xA) (srA _ yA) => fxA fyA; rewrite !LfV//. split. move => le1; apply /iorder_gle0P => //;apply /order_product_gleP; split => //. move => i idg; rewrite /f/cst_graph !LgV//. move: le1; rewrite /gle/related rb => le1. exact: (setIb_hi le1 idg). move => h; move :(iorder_gle1 h); move /order_product_gleP => [_ _ ali]. rewrite /gle/related rb; apply: setIb_i. case: (emptyset_dichot (domain g)) => neg. by case: nz; rewrite - cdg neg cardinal_set0. by apply /domain_set0P. move => i idg; move: (ali _ idg); rewrite /f/cst_graph !LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)