proposition: Lemma scale_subset_or : forall a y z:E, scale_subset y a -> scale_subset z a -> (sub y z) \/ (sub z y).
proof: Proof. ir. uh H. uh H0. ee. ap show_sub_or. ir. nin H5. nin H6. rwi inc_complement H5. rwi inc_complement H6. ee. uh H; ee. uh H; ee. assert (leq a y0 y1 \/ leq a y1 y0). ap H10. ap H2. am. ap H1; am. nin H11. ap H8. ap (H3 y0 y1). am. am. ap H7. ap (H4 y1 y0). am. am. Qed.
imports: Arith order