proposition: Lemma suborder_fixU_prop x: suborder_fix x -> sub x suborder_fix_max.
proof: Proof. move =>[pa pb] t tx; apply/setU_P; exists x => //. by apply:Zo_i; [ apply/setP_P | rewrite pb]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)