proposition: Lemma R2_decr_0 n : forall h h', R2 n h h' -> T1.lt (m h') (m h).
proof: Proof. Proof with auto with T1. induction 1 using R2_ind2 with (P0 := fun s s' (H : S2 n s s') => T1.lt (ms s') (ms s))... - repeat rewrite m_ms. now apply S1_decr with n. - now repeat rewrite m_ms. - apply oplus_strict_mono_l ... - repeat rewrite ms_eqn2. apply oplus_strict_mono_r... Qed.
imports: hydras(E0 Hessenberg)