proposition: Lemma avatar_image : forall f g u, is_leq_gen_scale f u -> Image.create u (avatar f g) = range (lgmap f g u).
proof: Proof. ir. rw lgmap_avatar_create. rw Function.create_range. ap Image.same. tv. ir. tv. am. Qed.
imports: Arith order