proposition: Lemma suborder_fixI_prop x: suborder_fix x -> sub suborder_fix_min x.
proof: Proof. move =>[pa pb] t ti. have xI: inc x (Zo (\Po E) (fun x => sub (g x) x)). by apply: Zo_i; [apply/setP_P | rewrite pb]. exact: (setI_hi ti xI). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)