proposition: Lemma is_suborder_trans : forall a b c : E, is_suborder a b -> is_suborder b c -> is_suborder a c.
proof: Proof. ir. ap show_is_suborder. ufi is_suborder H; xe. ufi is_suborder H0; xe. ir. apply is_suborder_leq with b. am. apply is_suborder_leq with a. exact H. exact H1. Qed.
imports: universe