proposition: Lemma downward_lgs_inc_refl :forall (f:E1)(x:E), leq_gen f x x -> inc x (downward_lgs f x).
proof: Proof. ir. pose (u:= choose_lgs_containing f x). assert (inc x u). rwi leq_gen_char H; ee. cp (choose_pr H); cbv beta in H1; ee; am. ee. uf downward_lgs. ap Z_inc. am. am. Qed.
imports: Arith order