proposition: Lemma stratified_fct_pr x (f := stratified_fct): W x -> f x = H x (Lg (stratified_set (idx x)) f).
proof: Proof. have H2: forall x, W x -> f x = H x (unionf (idx x) stratified_fct_aux). move => t wt; move: (OS_idx wt) => oi. rewrite /f/stratified_fct (stratified_fct_aux_p1 oi); rewrite LgV //. by apply /(stratified_setrP oi). move => wx; rewrite (H2 _ wx); apply: f_equal. have oi := OS_idx wx. have ha: forall t, ordinalp t -> sgraph (stratified_fct_aux t). move => t ot u ;rewrite (stratified_fct_aux_p1 ot). move/funI_P => [w wa ->]; fprops. have hb: sgraph (unionf (idx x) stratified_fct_aux). by move => y /setUf_P [z za]; apply: (ha _ (Os_ordinal oi za)). have hc: stratified_set (idx x) = domain (unionf (idx x) stratified_fct_aux). set_extens t. move => /(stratified_setP oi) [h1 h2] ; apply/(domainP hb). have oit:= (proj31_1 h2). have : inc t (domain (stratified_fct_aux (idx t))). rewrite (stratified_fct_aux_p1 oit); aw; apply/(stratified_setrP oit). by split. move/(domainP (ha _ oit)) => [y ya]; exists y. by apply/setUf_P; exists (idx t) => //; apply/(oltP). move => /(domainP hb) [y /setUf_P [z zi]]. have oz := (Os_ordinal oi zi). rewrite (stratified_fct_aux_p1 oz). move => /funI_P [u /(stratified_setrP oz) [wu iz] /pr1_def ->]. by apply/(stratified_setP oi); split => //; rewrite iz; apply/(oltP). have hbb: fgraph (unionf (idx x) stratified_fct_aux). split; first by exact. move => u v /setUf_P [y1 y1x y1v] /setUf_P [y2 y2x y2v]. move: (Os_ordinal oi y1x) (Os_ordinal oi y2x) => oy1 oy2. move: y2v; rewrite (stratified_fct_aux_p1 oy2). move: y1v; rewrite (stratified_fct_aux_p1 oy1). move => /funI_P [z1 z1i z1v] /funI_P [z2 z2i z2v]. move /(stratified_setrP oy1): z1i => [wz1 iz1]. move /(stratified_setrP oy2): z2i => [wz2 iz2]. by rewrite z1v z2v - iz1 - iz2; aw => ->. symmetry;apply:fgraph_exten. + fprops. + exact. + by aw. + aw => t ts; rewrite LgV//;move/(stratified_setP oi):ts => [Wt lt1]. have oit:= (proj31_1 lt1). have h := (stratified_fct_aux_p1 oit). have pa: inc t (stratified_setr (idx t)). by apply/(stratified_setrP oit). rewrite /f /stratified_fct. set u := Vg (stratified_fct_aux (idx t)) t. have pb: fgraph (stratified_fct_aux (idx t)) by rewrite h; fprops. have pc: inc t (domain (stratified_fct_aux (idx t))) by rewrite h; aw. move: (fdomain_pr1 pb pc); rewrite -/u => sa. have sb: inc (J t u) (unionf (idx x) stratified_fct_aux). by apply/setUf_P; exists (idx t) => //;apply/(oltP oi). by move: (pr2_def (in_graph_V hbb sb)); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)