proposition: Lemma olex_nsve x y: inc x (prod_of_substrates g) -> inc y (prod_of_substrates g) -> ((x = y) <-> (olex_nsv r x y = emptyset)).
proof: Proof. move=> px py;split. by move => ->; apply /set0_P=> t /Zo_P [pa]; case. have pd: order_fam g by move: ax=> [_ _]. have sd: substrate r = domain g by move: ax => [_]. move=> oe; move: px => /prod_of_substratesP [ra rb _]. move: py => /prod_of_substratesP [rd re _]. apply: fgraph_exten =>//; first by ue. by rewrite rb - sd => z zd; ex_middle sv; empty_tac1 z; apply /Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)