proposition: Lemma next_comp_sub_scale : forall (f:E1) (a b:E), next_compatible f a -> next_compatible f b -> (sub (U a) (U b)) -> scale_subset (U a) b.
proof: Proof. ir. cp (max_comp_scale_or H H0). nin H2. wr H2. assert (scale_bisubset a b (max_comp_scale a b)). ap max_comp_scale_bisubset. uh H; ee; am. uh H0; ee; am. uh H3; ee; am. assert (scale_bisubset a b (max_comp_scale a b)). ap max_comp_scale_bisubset. uh H; ee; am. uh H0; ee; am. uh H3; ee. rwi H2 H5. uh H5; ee. assert (U a = U b). apply extensionality; am. rw H10. wr H2. am. Qed.
imports: Arith order