proposition: Lemma S0_decr_0 : forall s s', S0 s s' -> T1.lt (ms s') (ms s).
proof: Proof. Proof with auto with T1. induction 1. - rewrite ms_eqn2; apply oplus_lt2... - repeat rewrite ms_eqn2; apply oplus_strict_mono_r ... Qed.
imports: hydras(E0 Hessenberg)