proposition: Lemma leq_gen_mapping_sub : forall f g r s, is_leq_gen_mapping f g r -> is_leq_gen_mapping f g s -> sub (domain r) (domain s) -> sub r s.
proof: Proof. ir. uh H; uh H0; ee. cp (leq_gen_scale_or H H0). nin H4; try am. util (function_sub_eq (r:=s)(s:=r)). am. am. am. am. rw H5. uhg; ir; am. Qed.
imports: Arith order