proposition: Lemma ns_restrAB_prop1 r (p:= ns_restrAB r): inc r ns_extensions -> forall x y, gle r x y <-> [/\ inc x C, inc y C & [\/ [/\ (Q x) = C0, Q y = C0 & gle rA (P x) (P y)], [/\ (Q x) = C0, Q y = C1 & p (P x) (P y)], [/\ (Q x) = C1, Q y = C0 & ~p (P y) (P x)] | [/\ (Q x) = C1, Q y = C1 & gle rB (P x) (P y)]]].
proof: Proof. move => /ns_extensions_prop2 [ha [or sr] tor] x y. move: wor1 =>[wo1 sr1]; move:(proj2 (worder_total wo1)); rewrite sr1 => tr1. move: wor2 =>[wo2 sr2]; move:(proj2 (worder_total wo2)); rewrite sr2 => tr2. split. move => le1. have aux: gle r y x -> x = y by move => hb; move:(proj44 or _ _ le1 hb). have xC: inc x C by rewrite - sr; order_tac. have yC: inc y C by rewrite - sr; order_tac. split => //. move/candu2P: (xC) => [px xC1]; move/candu2P: (yC) => [py yC1]. case: xC1; case: yC1. - move => [qa qb] [qc qd]; constructor 1; split => //. case:(tr1 _ _ qa qc) => // lab. have: inc (J y x) ns_compare. by apply/graph_on_P1; split => //; left. by move/ha /aux => eq1; move: lab; rewrite eq1. - move => [qa qb] [qc qd]; constructor 2; split => //. by rewrite /p /ns_restrAB -qd -qb px py. - move => [qa qb] [qc qd]; constructor 3; split => //. rewrite /p /ns_restrAB -qd -qb px py => /aux eq1. by move: C0_ne_C1; rewrite -qb - qd eq1. - move => [qa qb] [qc qd]; constructor 4; split => //. case:(tr2 _ _ qa qc) => // lab. have: inc (J y x) ns_compare. move: C1_ne_C0 => hh. by apply/graph_on_P1; split => //; right; rewrite qb qd. by move/ha /aux => eq1; move: lab; rewrite eq1. move =>[xC yC]; case. - by move => [pa pb pc]; apply: ha; apply/graph_on_P1; split => //; left. - move => [pa pb]; rewrite /p/ns_restrAB -pa -pb. by move/candu2P:xC =>[-> _]; move/candu2P:yC =>[-> _]. - move => h;move: (proj2 tor); rewrite sr=> h1; case: (h1 _ _ xC yC) => //. move:h => [pa pb]; rewrite /p/ns_restrAB -pa -pb. by move/candu2P:xC =>[-> _]; move/candu2P:yC =>[-> _]. - move => [pa pb pc]; apply: ha; apply/graph_on_P1; split => //; right. by move: C1_ne_C0 => hh; rewrite pa pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)