proposition: Lemma leq_gen_mapping_tack_on : forall f g r, is_leq_gen_mapping f g r -> ~inc (f (domain r)) (domain r) -> is_leq_gen_mapping f g (tack_on r (tandem f g r)).
proof: Proof. ir. uhg; ee. ap leq_gen_scale_tack_on. uh H; ee; am. uhg; ir. uh H; ee. cp (Function.lem2 H2 H1). ap H0. ufi tandem H3. rwi pr1_pair H3. am. uf tandem. ap function_tack_on_axioms. uh H; ee; am. am. Qed.
imports: Arith order