proposition: Lemma scale_subset_is_leq_gen_scale : forall (f:E1)(a y:E), next_compatible f a -> scale_subset y a -> is_leq_gen_scale f y.
proof: Proof. ir. uhg. sh (suborder y a). ee. uf suborder. rw underlying_create. tv. uhg; ee. ap suborder_well_ordered. uh H0; ee; am. uh H; ee; am. ir. assert (punctured_downward_subset (suborder y a) y0 = punctured_downward_subset a y0). ap extensionality; uhg; ir. uf punctured_downward_subset. ufi punctured_downward_subset H2. Ztac. ap Z_inc. uh H0; ee. ap H5. assert (U (suborder y a) = y). uf suborder; ap underlying_create. wr H7; am. uh H4; ee. uhg; ee; au. rwi leq_suborder_all H4. ee. am. uh H; ee; uh H; ee; uh H; ee; am. uh H0; ee; am. uf punctured_downward_subset. ufi punctured_downward_subset H2. Ztac. ap Z_inc. ufi suborder H1. rwi underlying_create H1. uf suborder; rw underlying_create. uh H0; ee. apply H6 with y0. am. uh H4; ee; am. uh H4; ee. uhg; ee; try am. rw leq_suborder_all; ee. uh H0; ee. apply H7 with y0; try am. ufi suborder H1; rwi underlying_create H1; am. ufi suborder H1; rwi underlying_create H1; am. am. uh H; ee; uh H; ee; uh H; ee; am. uh H0; ee; am. rw H2. uh H; ee. ap H3. uh H0; ee. ap H4. ufi suborder H1; rwi underlying_create H1; am. Qed.
imports: Arith order