proposition: Lemma chenille_tack_on : forall (f:E1)(x:E), leq_gen f x x -> tack_on (chenille f x) x = downward_lgs f x.
proof: Proof. ir. ap extensionality; uhg; ir. rwi tack_on_inc H0. nin H0. ufi chenille H0. Ztac. rw H0. ap downward_lgs_inc_refl. am. apply by_cases with (x0 = x); ir. rw tack_on_inc. ap or_intror; am. rw tack_on_inc; ap or_introl. uf chenille; ap Z_inc. am. am. Qed.
imports: Arith order