proposition: Lemma same_leq_eq : forall a b x y : E, same_order a b -> leq a x y = leq b x y.
proof: Proof. ir. ap iff_eq; ir. ufi same_order H. ee. apply is_suborder_leq with a; am. ufi same_order H; ee. apply is_suborder_leq with b; am. Qed.
imports: universe