proposition: Lemma scale_suborder_inclusion : forall a b : E, scale_subset a b -> is_scale (suborder_inclusion a b).
proof: Proof. ir. ufi scale_subset H; ee. ufk is_well_ordered H. ee. ufk is_linear H; ee. ufk axioms H; ee. uf is_scale; dj. ap suborder_inclusion_mor_axioms. am. am. uf injective. dj. ufi mor_axioms H8; ee. ufi strong_axioms H10; ee. exact H10. uf Transformation.injective. rw source_suborder_inclusion. rw target_suborder_inclusion. rw underlying_suborder. dj. uf Transformation.axioms. ir. rw ev_suborder_inclusion. ap H0; am. am. uf Transformation.injects. ir. rwi ev_suborder_inclusion H13; try am. rw H13. rw ev_suborder_inclusion. tv. am. rw source_suborder_inclusion. ap suborder_well_ordered. am. am. rw target_suborder_inclusion. am. sh y. dj. rw source_suborder_inclusion. rw underlying_suborder. apply H1 with x. rwi source_suborder_inclusion H12. rwi underlying_suborder H12. exact H12. rwi target_suborder_inclusion H13. rwi ev_suborder_inclusion H13. exact H13. rwi source_suborder_inclusion H12. rwi underlying_suborder H12. exact H12. rw ev_suborder_inclusion. tv. rwi source_suborder_inclusion H14. rwi underlying_suborder H14. exact H14. Qed.
imports: universe