proposition: Lemma ns_extensions_prop1 z: inc z ns_extensions <-> sub ns_compare z /\ worder_on z C.
proof: Proof. split. move => /Zo_P[/setP_P ha [hb hc]];split => //; split => //. set_extens t. by move/(order_reflexivityP (proj1 hc)) => ti; case/setXp_P: (ha _ ti). move => tC. suff: inc (J t t) ns_compare by move/hb => ti; substr_tac. by move: ns_order1 => [qa qb]; order_tac; ue. move => [qa [qb qc]]; apply: Zop_i => //; rewrite - qc. apply: (sub_graph_coarse_substrate (proj41 (proj1 qb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)