proposition: Lemma leq_gen_def_from_scale : forall f x, (exists u, is_leq_gen_scale f u & inc x u) -> leq_gen f x x.
proof: Proof. ir. nin H. ee. uh H. nin H. ee. rewrite weak_leq_gen_leq with (a:= x1). ap leq_refl. uh H1; ee. uh H1; ee. uh H1; ee. am. rw H; am. am. rw H; am. Qed.
imports: Arith order