proposition: Lemma ns_order1: order_on ns_compare C.
proof: Proof. move: wor1 =>[[or1 _] sr1]. move: wor2 =>[[or2 _] sr2]. have rr a :inc a C -> ns_compare_r a a. move=> /candu2P [pa h]; case: h =>- [ha hb]. left; split => //; order_tac; ue. have hh: Q a <> C0 by rewrite hb; fprops. right; split => //; order_tac; ue. have esr: substrate ns_compare = C by apply: graph_on_sr. split => //. apply: order_from_rel1. - move => w u v; case => -[ha hb hc];case => -[ha' hb' hc']. + left;split => //; order_tac. + by case: ha'. + by case: ha. + right; split => //; order_tac. - move => u v /candu2P [pa qa] /candu2P [pb qb]. case => -[ha hb hc];case => -[ha' hb' hc']. + apply: (pair_exten pa pb); [ order_tac | by rewrite ha hb]. + by case: ha'. + by case: ha. + apply: (pair_exten pa pb); first by order_tac. case: qa; first by move => [_ w]; case:ha. by move=> /proj2 ->; case qb => - [_]. - exact. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)