proposition: Lemma extension_osr E F: order_on (extension_order E F) (sub_functions E F).
proof: Proof. split; last by apply: graph_on_sr => a /sfunctionsP [pa pb pc]; split; fprops. apply: order_from_rel;split. - move=> a b c [fa fb gba tba] [fc _ gcb tcb]. split => //; [ by apply: sub_trans gba | by apply: sub_trans tba ]. - move=> a b [fb fa gba tba] [_ _ gab tab]. have grab: graph a = graph b by apply: extensionality. have tgab: target a = target b by apply: extensionality. by apply: function_exten1. - move => a b [fa fb _ _ ]; split; split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)