proposition: Theorem Rn_decrease : forall n u h h', Rn n u h h' -> h2o h' < h2o h.
proof: Proof. intros n o h h' H. elim H using Rn_rect2 with (P0 := fun o (h h0: Hydrae)(H:Sn n o h h0) => exists a, ltM a (h2ol h0) (h2ol h)). simpl;intros. case (S2_decrease _ _ _ _ s). intros. eapply ltM_lt with x. apply sort_nf. apply h2ol_nfs. apply sort_nf. apply h2ol_nfs. eapply ltM_equiv_ltM. 2:eapply sort_equiv. eapply ltM_equiv_ltMR. 2:eapply sort_equiv. auto. intros. case H0;intros a Ha. apply ltM_lt with a;auto. apply h2o_nf. apply h2o_nf. simpl. eapply ltM_equiv_ltM. 2:eapply sort_equiv. eapply ltM_equiv_ltMR. 2:eapply sort_equiv. auto. intros. exists (h2o h0). simpl. apply ltM_head. auto . intros. exists (h2o h0). simpl;apply ltM_head. auto with arith. intros. case H0. intros. exists x. simpl;apply ltM_cons;auto. Qed.
imports: Arith Omega List EPSILON0 MSE0