proposition: Lemma R1_decr_0 : forall h h', R1 h h' -> T1.lt (m h') (m h).
proof: Proof. Proof with auto with T1. destruct 1; simpl; destruct s, s'. - inversion H. - inversion H. - rewrite ms_eqn2; apply lt_le_trans with (T1.phi0 (m h))... + apply oplus_le1 ... - now apply S0_decr. Qed.
imports: hydras(E0 Hessenberg)