proposition: Lemma create_little_leq : forall a : E, is_order_on a -> a = create x (little_leq (lit_lq a)).
proof: Proof. ir. assert (leq a = little_leq (lit_lq a)). ap arrow_extensionality; intro u. ap arrow_extensionality; intro v. ap iff_eq; ir. ufk leq H0; ee. ufk is_order_on H; ee. uhg; ee. wr H3; am. wr H3; am. ir. uhg. rw B_eq. rw B_eq. am. ufi little_leq H0; ee. cp (H2 H0 H1). ufi lit_lq H3. rwi B_eq H3. rwi B_eq H3. am. wr H0. uh H. ee. wr H1. exact H2. Qed.
imports: universe