proposition: Lemma leq_gen_mapping_exists : forall f g u, is_leq_gen_scale f u -> exists r, lgmaps f g u r.
proof: Proof. intros f g. util (lgs_induction (f:=f) (p:= fun u=> exists r, (lgmaps f g u r))); ir. pose (pool := Image.create z (lgmap f g)). pose (r:= union pool). sh r; uhg; ee; ir. uf r. ap leq_gen_mapping_union. ir. ufi pool H0. rwi Image.inc_rw H0. nin H0. ee. cp (H _ H0). cp (lgmaps_exists_pr H2). rwi H1 H3. uh H3; ee; am. uf r; rw domain_union. ap extensionality; uhg; ir. cp (union_exists H0). nin H1; ee. rwi Image.inc_rw H2. nin H2; ee. ufi pool H2. rwi Image.inc_rw H2; nin H2; ee. cp (H _ H2). cp (lgmaps_exists_pr H5). rwi H4 H6. uh H6; ee. apply union_inc with x0. am. wr H3; rw H7; am. cp (union_exists H0). nin H1; ee. apply union_inc with x0. am. rw Image.inc_rw. sh (lgmap f g x0). ee. uf pool. rw Image.inc_rw. sh x0. ee; try am; try tv. cp (H _ H2). cp (lgmaps_exists_pr H3). uh H4; ee; am. apply by_cases with (inc (f u) u); ir. nin H. sh x. assert (tack_on u (f u) = u). ap extensionality; uhg; ir. rwi tack_on_inc H1; nin H1. am. rw H1; am. rw tack_on_inc; ap or_introl; am. rw H1; am. nin H. sh (tack_on x (tandem f g x)). uhg; ee. ap leq_gen_mapping_tack_on. uh H; ee; am. uh H; ee. rw H1. am. uf tandem. rw domain_tack_on. uh H; ee. rw H1; tv. ap H. am. Qed.
imports: Arith order