proposition: Lemma fo_gle1P x u v: gle (finer_order x) u v <-> [/\ order u, order v, substrate u = x, substrate v = x & forall a b, inc a x -> inc b x -> gle u a b -> gle v a b].
proof: Proof. split. move /fo_gleP => [ou ov su sv h]; split => //. by move=> a b ax bx ab; apply: h. move => [ou ov su sv h]; apply /fo_gleP;split => //. have gu: (sgraph u) by fprops. move=> t tu. have pt : (pairp t) by apply: gu. move: tu;rewrite -pt => tu. have p1: (inc (P t) x) by rewrite - su; substr_tac. have p2: (inc (Q t) x) by rewrite - su; substr_tac. by apply: (h _ _ p1 p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)