proposition: Lemma max_is_subset : forall (f:E1)(x:E), (sub (max_leq_gen_scale f x) x).
proof: Proof. ir. uhg; ir. ufi max_leq_gen_scale H. cp (union_exists H). nin H0; ee. Ztac. cp (powerset_sub H2). ap H4; am. Qed.
imports: Arith order