proposition: Lemma leq_gen_is_next: forall (f:E1)(x y:E), leq_gen f x y -> x = y \/ exists u:E, (is_leq_gen_scale f u & inc x u & y = f u).
proof: Proof. ir. apply by_cases with (x=y); ir. ap or_introl; am. ap or_intror. cp H. uh H1. nin H1. ee. sh (punctured_downward_subset x0 y). ee. apply scale_subset_is_leq_gen_scale with x0. am. ap punctured_downward_scale; try am. uh H1; ee; am. uh H2; ee; am. uf punctured_downward_subset; ap Z_inc; ee. uh H2; ee; am. uhg; ee; am. uh H1; ee. sy. ap H3. uh H2; ee; am. Qed.
imports: Arith order