proposition: Lemma S1_decr_0 n: forall s s', S1 n s s' -> T1.lt (ms s') (ms s).
proof: Proof. Proof with auto with T1. induction 1. - rewrite ms_eqn2. simpl hcons_mult. rewrite ms_eqn2. rewrite ms_eqn3. rewrite oplus_assoc... apply oplus_strict_mono_l... apply oplus_nf... apply o_finite_mult_nf... rewrite <- o_finite_mult_S_rw. apply o_finite_mult_lt_phi0_1. now apply R1_decr. apply o_finite_mult_nf... - repeat rewrite ms_eqn2 ... apply oplus_strict_mono_r ... Qed.
imports: hydras(E0 Hessenberg)