proposition: Lemma max_is_max : forall (f:E1)(x u:E), is_leq_gen_scale f u -> sub u x -> sub u (max_leq_gen_scale f x).
proof: Proof. ir. uhg; ir. uf max_leq_gen_scale. apply union_inc with u. am. ap Z_inc. ap powerset_inc; am. am. Qed.
imports: Arith order