proposition: Lemma leq_gen_scale_subset : forall (f:E1)(a y:E), next_compatible f a -> is_leq_gen_scale f y -> sub y (U a) -> scale_subset y a.
proof: Proof. ir. uh H0; nin H0; ee. wr H0. apply next_comp_sub_scale with f. am. am. rw H0; am. Qed.
imports: Arith order