proposition: Lemma order_function_osr: order_on (order_function x y r)(functions x y).
proof: Proof. have gf: sgraph (order_function x y r) by apply: graph_on_graph. have rr:forall u, inc u (functions x y) -> gle (order_function x y r) u u. move=> u us; apply: Zo_i; rewrite /coarse;fprops. aw; move /functionsP: us => [fu su tu]. split => // i ix; order_tac. rewrite sr -tu; rewrite - su in ix; fprops. have sr1: substrate (order_function x y r) = functions x y. set_extens t. by case/(substrate_P gf) => [] [z] /Zo_P [] /setXp_P []. by move => /rr/arg1_sr. split => //; split. rewrite /order_function;apply: graph_on_graph. by move=> z zs; apply: rr;rewrite - sr1. move=> a b c/order_functionP [afs bfs leab] /order_functionP [_ cfs lebc]. apply/order_functionP;split=> //. move=> i id; move: (leab _ id) (lebc _ id) => lab lbc; order_tac. move=> a b /order_functionP [afs bfs leab] /order_functionP [_ _ leba]. move: afs bfs => /functionsP [fa sa ta] /functionsP [fb sb tb]. apply: function_exten=>//; try ue. rewrite sa; move=> i ix;move: (leab _ ix) (leba _ ix)=> lab lba; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)