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