proposition: Lemma same_order_trans : forall a b c : E, same_order a b -> same_order b c -> same_order a c.
proof: Proof. ir. ufi same_order H. ufi same_order H0. uf same_order. ee. apply is_suborder_trans with b. exact H. exact H0. apply is_suborder_trans with b. exact H1. exact H2. Qed.
imports: universe