proposition: Lemma inductive_graphs a b: inductive (opp_order (extension_order a b)).
proof: Proof. move: (extension_osr a b)=> [or sr]. move: (opp_osr or) => [ooi osr] X XX. move: (XX); rewrite osr sr => Xs toX. have Ha:forall i, inc i X -> function i. by move=> i iX; move: (Xs _ iX) => /sfunctionsP []. have Hb:forall i, inc i X -> target i = b. by move=> i iX; move: (Xs _ iX) => /sfunctionsP [_ ]. move: toX=> [orX]; rewrite iorder_sr // => tor. set si:= Lg X source. have Hd: forall i j, inc i (domain si) -> inc j (domain si) -> agrees_on ((Vg si i) \cap (Vg si j)) i j. rewrite /si; aw; move=> i j iX jX; rewrite !LgV //. split; [by apply: subsetI2l | by apply: subsetI2r | ]. move=> t /setI2_P [ti tj]. case: (tor _ _ iX jX) => h; move: (iorder_gle1 h)=> h'. apply: (extension_order_pr h' ti). symmetry; apply: (extension_order_pr h' tj). have He:forall i, inc i (domain si) -> function_prop i (Vg si i) b. rewrite /si; aw; move=> i iX; rewrite LgV //;split; fprops. move: (extension_covering He Hd) => [[fg sg tg] _ _ agg]. set g:= (common_ext si id b). have gs: (inc g (sub_functions a b)). apply /sfunctionsP;split => // t tsg. rewrite sg in tsg; move: (setUf_hi tsg)=> [v]. rewrite {1}/si; aw => vx; rewrite LgV // => tv. by move: (Xs _ vx) => /sfunctionsP [_ sv _]; apply: sv. rewrite /upper_bound osr sr; ex_tac. move: agg; rewrite /si; aw => agg. move=> y yX; move: (Xs _ yX)=> ys; move: (agg _ yX)=> ag. have fy: (function y) by move: ys; fprops. apply /igraph_pP; apply/extension_order_P1;split => //. apply/(sub_functionP fy fg). move: ag; rewrite /agrees_on !LgV //;move=> [p1 p2 p3]; split => //. by move=> u; symmetry; apply: p3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)