proposition: Lemma max_f_out : forall (f:E1)(x:E), let u := max_leq_gen_scale f x in ~inc (f u) (complement x u).
proof: Proof. ir. uhg; ir. pose (v:=tack_on u (f u)). assert (~inc (f u) u). ufi complement H. Ztac. assert (inc v (powerset x)). ap powerset_inc. uf v. uhg; ir. rwi tack_on_inc H1. nin H1. assert (sub u x). uf u; ap max_is_subset. ap H2. am. rw H1. ufi complement H. Ztac. assert (is_leq_gen_scale f v). uf v. ap leq_gen_scale_tack_on. uf u; ap max_is_leq_gen_scale. am. assert (sub v u). uf u. ap max_is_max. am. exact (powerset_sub H1). ap H0. ap H3. uf v. rw tack_on_inc. ap or_intror; tv. Qed.
imports: Arith order