proposition: Lemma coinciders_saturated : forall a b c : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> downward_saturated a b (coinciders a b c).
proof: Proof. ir. uhg. dj. uh H; ee. uh H; ee. uh H; ee. am. uh H; ee. uh H; ee. uh H; ee. am. uhg; ir. ufi coinciders H3; Ztac. uf coinciders; ap Z_inc. am. uhg; ee. am. ufi coinciders H4. Ztac. uh H8; ee. au. ir. ufi coinciders H4; Ztac. uh H10. ee. ap H12. am. uh H1; ee. apply H17 with y. am. am. ir. ufi coinciders H4. Ztac. uh H10; ee. ap H13. am. uh H1; ee. apply H17 with y. am. am. Qed.
imports: universe