proposition: Lemma chenille_next : forall (f:E1)(x:E), leq_gen f x x -> f (chenille f x) = x.
proof: Proof. ir. cp H; uh H. nin H. ee. rewrite chenille_punctured_downward with (a:=x0). uh H; ee. ap H2. uh H1; ee; am. am. uh H1; ee; am. Qed.
imports: Arith order