proposition: Lemma leq_create_all : forall a b : E, leq create a b = A (inc a x) (A (inc b x) (lq a b)).
proof: Proof. ir. ap iff_eq. uf leq. rw underlying_create. ir; ee. am. am. rwi less_than_rw H1. nin H1. exact (B H1). am. am. ir. rw leq_create; ee; am. Qed.
imports: universe