proposition: Lemma order_functionP f f': gle (order_function x y r) f f' <-> [/\ inc f (functions x y), inc f' (functions x y) & forall i, inc i x -> gle r (Vf f i) (Vf f' i)].
proof: Proof. split; first by move /Zo_P => [/setXp_P [pa pb]]; aw; move => [_ _ bb]. move => [pa pb pc];apply:Zo_i; first by apply:setXp_i. move/functionsP: pa => pa. move/functionsP: pb => pb. by hnf; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)