proposition: Lemma chenille_inc : forall (f:E1)(x y:E), leq_gen f x x -> inc y (chenille f x) = (leq_gen f y x & y<>x).
proof: Proof. ir. ap iff_eq; ir. ufi chenille H0; Ztac. rwi downward_lgs_inc H1; try am. uf chenille; ap Z_inc. rw downward_lgs_inc; xd. ee; am. Qed.
imports: Arith order