proposition: Lemma leq_gen_scale_or : forall (f:E1)(y z:E), is_leq_gen_scale f y -> is_leq_gen_scale f z -> (sub y z \/ sub z y).
proof: Proof. ir. uh H; uh H0; nin H; nin H0. ee. cp (next_compatible_or H1 H2). nin H3. ap or_intror. wr H; wr H0. uh H3; ee; am. ap or_introl. wr H; wr H0. uh H3; ee; am. Qed.
imports: Arith order