proposition: Lemma maximal_extensionP E F x: nonempty F -> inc x (sub_functions E F) -> (maximal (opp_order (extension_order E F)) x <-> (source x = E)).
proof: Proof. have [eo es]:= (extension_osr E F). move=> [t tF] xs; apply: (iff_trans (maximal_opp eo _)). split. move: (xs) => /sfunctionsP [fx sx tx][_ h]. apply: extensionality=>// y yE. ex_middle yns. have aux: gle (extension_order E F) (extension x y t) x. rewrite /extension;apply /extension_order_P1; split=> //;last by aw; fprops. apply /sfunctionsP; split => //; aw. - apply: extension_f => //. - by move => z /setU1_P; case; [apply: sx |move=>->]. - rewrite - tx; apply /setU2id_Pr => s /set1_P ->; ue. by rewrite -(h _ aux); rewrite /extension; aw; fprops. move=> sx. hnf; aw; split; first by ue. move=> y /extension_orderP [ys _ et]. move: xs ys => /sfunctionsP [fx _ tx] /sfunctionsP [fy sy ty]. have sy' := (extends_Ssource et). symmetry;apply: function_exten=>//; try ue. apply: extensionality=>//; ue. move=> z zs /=; apply: (extends_sV et zs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)