proposition: Lemma chenille_punctured_downward : forall (f:E1)(a x:E), next_compatible f a -> inc x (U a) -> chenille f x = punctured_downward_subset a x.
proof: Proof. ir. ap extensionality; uhg; ir. rwi chenille_inc H1. ee. rewrite weak_leq_gen_leq with (a:= a) in H1. uf punctured_downward_subset; ap Z_inc. uh H1; ee; am. uhg; ee; am. am. am. rewrite weak_leq_gen_leq with (a:=a). ap leq_refl. do 3 (uh H; ee); am. am. am. am. rw chenille_inc. ee. rewrite leq_gen_leq with (a:=a). ufi punctured_downward_subset H1; Ztac. uh H3; ee; am. am. ufi punctured_downward_subset H1; Ztac. am. ufi punctured_downward_subset H1; Ztac. uh H3; ee; am. rewrite leq_gen_leq with (a:=a). ap leq_refl. do 3 (uh H; ee); am. am. am. am. am. Qed.
imports: Arith order