proposition: Lemma leq_gen_mapping_same_ev : forall f g r s x, is_leq_gen_mapping f g r -> is_leq_gen_mapping f g s -> inc x (domain r) -> inc x (domain s) -> V x r = V x s.
proof: Proof. ir. cp (leq_gen_mapping_domain H). cp (leq_gen_mapping_domain H0). cp (leq_gen_scale_or H3 H4). nin H5. pose (t:= restr s (domain r)). assert (V x s = V x t). uf t. sy. ap restr_ev. uh H0; ee; am. am. am. assert (t = r). apply leq_gen_mapping_unique with f g. uf t. ap leq_gen_mapping_restr. am. am. am. am. uf t. rw restr_domain. ap extensionality; uhg; ir. apply intersection2_second with (domain s); am. ap intersection2_inc. ap H5; am. am. uh H0; ee; am. wr H7. sy; am. pose (t:= restr r (domain s)). assert (V x r = V x t). uf t. sy. ap restr_ev. uh H; ee; am. am. am. assert (t = s). apply leq_gen_mapping_unique with f g. uf t. ap leq_gen_mapping_restr. am. am. am. am. uf t. rw restr_domain. ap extensionality; uhg; ir. apply intersection2_second with (domain r); am. ap intersection2_inc. ap H5; am. am. uh H; ee; am. wr H7. am. Qed.
imports: Arith order