proposition: Lemma ns_restrAB_prop2 r (p:= ns_restrAB r): inc r ns_extensions -> r = ns_compare \cup ns_extend (ns_restrAB r).
proof: Proof. move => h. move: (ns_restrAB_prop1 h) => p1. move:h => /ns_extensions_prop2 [ha [or sr] tor]. move: ns_order1 => [qa qb]. set_extens t. move => tr. move: (proj41 or t tr) => pt. move: tr; rewrite - pt; move/p1 =>[pC qC]; case; move=> [ra rb rc]. - by apply/setU2_P; left; apply/graph_on_P1; split => //; left. - apply/setU2_P; right; apply: Zo_i; first by apply: setXp_i. by left; aw. - apply/setU2_P; right; apply: Zo_i; first by apply: setXp_i. by right; aw. - apply/setU2_P; left; apply/graph_on_P1; split => //; right. by move: C1_ne_C0 => hh; rewrite ra rb. case/setU2_P. move=> /Zo_P [/setX_P [pt pta ptb]] => h; rewrite - pt; apply/p1. split => //; case:h => h; first by constructor 1. move: h =>[pa pb pc]. case:(candu2_pr2 pta) => // ->. case:(candu2_pr2 ptb) => // ->. by constructor 4. move => /Zo_P [/setX_P [pt pta ptb]] => h; rewrite - pt; apply/p1. split => //; case:h => h; [ by constructor 2 | by constructor 3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)