proposition: Lemma leq_gen_mapping_restr : forall f g r u, is_leq_gen_mapping f g r -> is_leq_gen_scale f u -> sub u (domain r) -> is_leq_gen_mapping f g (restr r u).
proof: Proof. ir. cp (lgmap_lgmaps g H0). util (leq_gen_mapping_sub (f:=f) (g:=g) (r:=(lgmap f g u))(s:= r)). uh H2; ee; am. am. rw lgmap_domain. am. am. assert (u = domain (lgmap f g u)). sy; ap lgmap_domain. am. rw H4. rw restr_to_domain. uh H2; ee; am. uh H2; ee. uh H2; ee. am. uh H; ee; am. am. Qed.
imports: Arith order