proposition: Lemma expansive_scale_chenille : forall f u, is_expansive f -> is_leq_gen_scale f u -> chenille f (f u) = u.
proof: Proof. ir. ap leq_gen_scale_chenille. am. sh (tack_on u (f u)). ee. ap leq_gen_scale_tack_on. am. uh H; ee. ap H. am. uhg; ee. uhg; uhg; ir. uh H. ap (H _ H0). set (v:= f u). rw H1; rw tack_on_inc; ap or_intror. tv. uhg; ir. rw tack_on_inc; ap or_introl; am. Qed.
imports: Arith order