proposition: Lemma avatar_chenille : forall f g x, is_expansive g -> leq_gen f x x -> chenille g (avatar f g x) = Image.create (chenille f x) (avatar f g).
proof: Proof. ir. rw avatar_image_chenille. rw expansive_scale_chenille. tv. am. ap lgs_avatar_image. ap chenille_leq_gen_scale. am. am. Qed.
imports: Arith order