proposition: Lemma suborder_trans : forall a b c : E, axioms c -> sub a b -> sub b (U c) -> same_order (suborder a (suborder b c)) (suborder a c).
proof: Proof. ir. uf same_order; ee; ap show_is_suborder. ap suborder_axioms. ap suborder_axioms. am. am. uf suborder; rw underlying_create. am. ap suborder_axioms. am. uf sub; ir; au. ir. ap leq_suborder_if. rwi leq_suborder_all H2. ee; am. ap suborder_axioms; am. uf suborder; rw underlying_create. am. rwi leq_suborder_all H2; ee. am. ap suborder_axioms; am. uf suborder; rw underlying_create. am. uf sub; ir; au. rwi leq_suborder_all H2; ee. rwi leq_suborder_all H4; ee. am. am. am. ap suborder_axioms; am. uf suborder; rw underlying_create; uf sub; ir; au. ap suborder_axioms. am. uf sub; ir; au. ap suborder_axioms. ap suborder_axioms; am. uf suborder; rw underlying_create. am. ir. rwi leq_suborder_all H2; ee. ap leq_suborder_if; au. uf suborder; rw underlying_create; am. ap leq_suborder_if. au. au. am. am. am. uf sub; ir; au. Qed.
imports: universe