proposition: Lemma greatest_extension E F x: greatest (opp_order (extension_order E F)) x -> nonempty E -> small_set F.
proof: Proof. move=> ge [t tE]. case: (emptyset_dichot F); first by move => ->; exact: small0. have [oe sr] :=(extension_osr E F). case: (opp_osr oe); set (r:= opp_order (extension_order E F)) => or sr' neF. have alc u: inc u F -> Vf x t = u. move=> uF. move: (constant_prop E uF) => [sa sb sc]. have fsf:inc (constant_function E F u) (sub_functions E F). apply /sfunctionsP;split => //. by rewrite sb. move/(maximal_extensionP neF fsf): sb => sF. by rewrite (greatest_unique_maximal ge sF) constant_V. by move => u v /alc <- /alc <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)