proposition: Lemma fo_gleP x u v: gle (finer_order x) u v <-> [/\ order u, order v, substrate u = x, substrate v = x & sub u v].
proof: Proof. split. by move /sub_gleP => [] /ordersP [pa pb] /ordersP [pd pe] pf. move => [pa pb pc pd pe]. by apply /sub_gleP;split => //; apply/ordersP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)