proposition: Lemma chenille_leq_gen_scale : forall (f:E1)(x:E), leq_gen f x x -> is_leq_gen_scale f (chenille f x).
proof: Proof. ir. pose (u:= downward_lgs f x). assert (is_leq_gen_scale f u). uf u; ap downward_lgs_lgs; am. cp H0. uh H0; nin H0. ee. assert (chenille f x = punctured_downward_subset x0 x). ap extensionality; uhg; ir. ufi chenille H3; Ztac. uf punctured_downward_subset; ap Z_inc. rw H0; am. uhg; ee; try am. rewrite <- leq_gen_leq with (f:=f). rwi downward_lgs_inc H4; am. am. rw H0; uf u; am. rw H0; uf u; ap downward_lgs_inc_refl. am. uf chenille; ap Z_inc. fold u. wr H0. ufi punctured_downward_subset H3; Ztac. ufi punctured_downward_subset H3; Ztac. uh H5; ee; am. rw H3. apply scale_subset_is_leq_gen_scale with x0. am. ap punctured_downward_scale. uh H2; ee; am. rw H0; uf u; ap downward_lgs_inc_refl; am. Qed.
imports: Arith order