proposition: Lemma full_cc_leq_gen_scale : forall x:E, is_leq_gen_scale (complementary_choice x) x.
proof: Proof. ir. cp (max_lgs_cc_full x). pose (f:= complementary_choice x). fold f. wr H. fold f. ap max_is_leq_gen_scale. Qed.
imports: Arith order