proposition: Lemma order_structure s a: inc s (\Po (coarse a)) -> s \cg s = s -> s \cap (inverse_graph s) = diagonal a -> a = substrate s.
proof: Proof. move => /setP_P pa pb pc; set_extens t => ta. have : inc (J t t) (diagonal a) by apply /diagonal_pi_P. rewrite -pc => /setI2_P [ts _]; substr_tac. have sg: sgraph s by rewrite - pb; fprops. by case /(substrate_P sg): ta => [] [y ps]; move: (pa _ ps) => /setXp_P [pd pe]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)