proposition: Lemma max_lgs_cc_full : forall x :E, max_leq_gen_scale (complementary_choice x) x = x.
proof: Proof. ir. pose (f:= complementary_choice x). pose (u:= max_leq_gen_scale f x). assert (~inc (f u) (complement x u)). exact (max_f_out (f:= f) (x:=x)). ap extensionality. uf u; ap max_is_subset. uhg; ir. ap excluded_middle; uhg; ir. ap H. uf f. uf complementary_choice. ap choose_pr. sh x0. uf complement; ap Z_inc. am. am. Qed.
imports: Arith order