proposition: Lemma subp_gleP E u v: gle (subp_order E) u v <-> [/\ sub u E, sub v E & sub u v].
proof: Proof. split; first by move /graph_on_P1 => [] /setP_P pa /setP_P pb. by move => [pa pb pc]; apply /graph_on_P1;split => //; apply/setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)