proposition: Lemma leq_gen_mapping_union : forall f g z, (forall r, inc r z -> is_leq_gen_mapping f g r) -> is_leq_gen_mapping f g (union z).
proof: Proof. ir. uhg; ee. ap leq_gen_scale_union. ir. cp (H _ H0). uh H1; ee; am. ap function_glueing. ir. cp (H _ H0). uh H1; ee; am. ir. cp (H _ H0); cp (H _ H1). uh H4; uh H5; ee. nin (leq_gen_scale_or H4 H5). ap function_sub_V; am. sy; ap function_sub_V; try am. Qed.
imports: Arith order