proposition: Lemma S_pred_rw (f : nat -> nat) : S <<= f -> forall x, S (Nat.pred (f x)) = f x.
proof: Proof. intros H x; case_eq (f x). - intro H0. specialize (H x); rewrite H0 in H. inversion H. - reflexivity. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)