proposition: Lemma avatar_inj : forall f g x y, is_expansive g -> leq_gen f x x -> leq_gen f y y -> (avatar f g x) = (avatar f g y) -> x = y.
proof: Proof. ir. rewrite <- avatar_inv with (f:=f) (g:= g). wr H2. rw avatar_inv. tv. am. am. am. am. Qed.
imports: Arith order