proposition: Lemma suborder_fixU: suborder_fix suborder_fix_max.
proof: Proof. rewrite /suborder_fix_max; set (A := Zo _ _). have su: (sub (union A) E). by apply: setU_s2 => y /Zo_P [q1 q2]; apply /setP_P. have p3: (forall x, inc x A -> sub x (g (union A))). move=> x /Zo_P [q1 q2];apply: (sub_trans q2); apply: gM =>//. by apply setU_s1; apply: Zo_i. have p4: (sub (union A) (g (union A))). by move=> t /setU_P [y ty yA]; move: (p3 _ yA) =>q; apply: q. split => //; apply: extensionality => //. move=> t tg;move: (gS su) => p5; move: (gM p4 p5) => p6. by apply: (setU_i tg); apply: Zo_i => //; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)