proposition: Lemma leq_gen_mapping_range : forall f g r, is_leq_gen_mapping f g r -> is_leq_gen_scale g (range r).
proof: Proof. intros f g. pose (p:= fun r => is_leq_gen_scale g (range r)). util (lgs_induction (f:=tandem f g) (p:=p)). ir. uf p; cbv beta. ee; ir. rw range_union. ap leq_gen_scale_union. ir. rwi Image.inc_rw H0; nin H0; ee. wr H1. cp (H _ H0). ufi p H2; cbv beta in H2; ee. am. ir. uf tandem. uf p; cbv beta. rw range_tack_on. apply by_cases with (inc (g (range u)) (range u)). ir. assert (tack_on (range u) (g (range u))= range 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. ufi p H; cbv beta in H. am. ir. ap leq_gen_scale_tack_on. ufi p H; cbv beta in H; am. am. ir. uh H0. ee. cp (H _ H0). am. Qed.
imports: Arith order