proposition: Lemma set1_order_is0 r x: order r -> substrate r = singleton x -> r = singleton (J x x).
proof: Proof. move=> or sxsu. apply: set1_pr; first by order_tac;rewrite sxsu; fprops. move=> v vx; move: (pr1_sr vx) (pr2_sr vx);rewrite sxsu. move => /set1_P {2} <- /set1_P <-. by rewrite ((order_sgraph or) _ vx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)