proposition: Lemma suborder_fixI: suborder_fix suborder_fix_min.
proof: Proof. rewrite /suborder_fix_min; set (A := Zo _ _). have iEA: inc E A by apply: Zo_i;[ apply/setP_P | apply: gS]. have neA: nonempty A by ex_tac. have p3 x: inc x A -> sub (g (intersection A)) x. move => xA; move /Zo_P: (xA)=> [/setP_P xE gg]; apply: sub_trans gg. by apply: (gM _ xE); apply: setI_s1. have p4: sub (g (intersection A)) (intersection A). by move => t tg; apply/(setI_P neA) => y /p3; apply. have siE := (setI_s1 iEA). have p5: inc (g (intersection A)) A. by apply: Zo_i; [ apply/setP_P; apply: gS | move: (gM p4 (setI_s1 iEA))]. split => //. apply: extensionality => // t tI; exact: (setI_hi tI p5). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)