proposition: Lemma leq_gen_mapping_avatar : forall f g r x, is_leq_gen_mapping f g r -> inc x (domain r) -> V x r = avatar f g x.
proof: Proof. ir. uf avatar. assert (lem1 : leq_gen f x x). ap leq_gen_def_from_scale. sh (domain r); ee; try am. apply leq_gen_mapping_domain with g. am. set (u:= chenille f x). set (s := lgmap f g u). assert (is_leq_gen_mapping f g s). uf s. ap lgmap_lgmapping. uf u. ap chenille_leq_gen_scale. assert (is_leq_gen_scale f (domain r)). apply leq_gen_mapping_domain with g. am. am. assert (is_leq_gen_mapping f g (tack_on s (tandem f g s))). ap leq_gen_mapping_tack_on. am. uf s. rw lgmap_domain. uf u. rw chenille_inc. uhg; ir. ee. ap H3. ap chenille_next. am. ap leq_gen_def_from_scale. sh (domain r); ee; try am. apply leq_gen_mapping_domain with g. am. uf u. ap chenille_leq_gen_scale. am. set (t:= tack_on s (tandem f g s)) in H2. assert (inc (pair x (g (range s))) t). uf t; rw tack_on_inc; ap or_intror. uf tandem. assert (x=f(domain s)). uf s. rw lgmap_domain. uf u. sy; ap chenille_next. am. uf u; ap chenille_leq_gen_scale; am. rw H3. tv. cp (Function.pr2_V (f:=t) (x:=(pair x (g (range s))))). rwi pr2_pair H4. rw H4. rw pr1_pair. apply leq_gen_mapping_same_ev with f g. am. am. am. uf t. uf tandem. rw domain_tack_on. rw tack_on_inc; ap or_intror. uf s. rw lgmap_domain. uf u. rw chenille_next. tv. am. uf u. ap chenille_leq_gen_scale. am. ufi t H2. uh H2; ee. am. uf t. rw tack_on_inc. ap or_intror. uf tandem. assert (x = f (domain s)). uf s. rw lgmap_domain; try am. uf u. rw chenille_next; try tv; try am. uf u. ap chenille_leq_gen_scale; try am. rw H5. tv. Qed.
imports: Arith order