proposition: Lemma leq_gen_scale_chenille : forall (f:E1)(u:E), is_leq_gen_scale f u -> (exists v:E, (is_leq_gen_scale f v & strict_sub u v)) -> chenille f (f u) = u.
proof: Proof. ir. nin H0. ee. uh H0; nin H0; ee. rewrite chenille_punctured_downward with (a:= x0). assert (f u = next x0 u). sy; ap next_compatible_scale. am. apply leq_gen_scale_subset with (f:=f). am. am. rw H0; uh H1; ee; am. rw H0; am. rw H3. ap scale_is_punctured_downward. apply leq_gen_scale_subset with (f:=f). am. am. rw H0; uh H1; ee; am. rw H0; am. am. assert (f u = next x0 u). sy; ap next_compatible_scale. am. apply leq_gen_scale_subset with (f:=f). am. am. rw H0; uh H1; ee; am. rw H0; am. rw H3. ap next_inc_U. rw H0; am. uh H2; ee; am. Qed.
imports: Arith order